From 028a8c4262db384eaa78db1bbc07518b0a156333 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Mon, 5 Feb 2024 15:15:39 +0100
Subject: [PATCH 1/8] Type check Function.Lift

Forgot to add this one previously.  It's not included in the
`Felix.Instances.Function` as the rest of the Function directory.
---
 src/Felix/All.agda                     | 1 +
 src/Felix/Instances/Function/Lift.agda | 6 +++---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Felix/All.agda b/src/Felix/All.agda
index 8837fe1..bfabf06 100644
--- a/src/Felix/All.agda
+++ b/src/Felix/All.agda
@@ -20,4 +20,5 @@ import Felix.Construct.Comma
 import Felix.Construct.Arrow
 
 import Felix.Instances.Function
+import Felix.Instances.Function.Lift
 import Felix.Instances.Identity
diff --git a/src/Felix/Instances/Function/Lift.agda b/src/Felix/Instances/Function/Lift.agda
index 1b89acc..1c6a551 100644
--- a/src/Felix/Instances/Function/Lift.agda
+++ b/src/Felix/Instances/Function/Lift.agda
@@ -7,7 +7,7 @@ module Felix.Instances.Function.Lift (a b : Level) where
 open Lift
 open import Data.Product using (_,_)
 
-open import Felix.Homomorphism hiding (refl)
+open import Felix.Homomorphism
 open import Felix.Object
 
 private module F {ℓ} where open import Felix.Instances.Function ℓ public
@@ -17,8 +17,8 @@ private
   variable
     A : Set a
 
-lift₀ : ⦃ _ : Products (Set (a ⊔ b)) ⦄ → A → (⊤ F.⇾ Lift b A)
-lift₀ n tt = lift n
+lift₀ : A → (⊤ F.⇾ Lift b A)
+lift₀ a tt = lift a
 
 lift₁ : (A F.⇾ A) → (Lift b A F.⇾ Lift b A)
 lift₁ f (lift a) = lift (f a)

From 994a5830d19a1200bbd522fbd8b690605a0aec34 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Mon, 5 Feb 2024 14:46:07 +0100
Subject: [PATCH 2/8] Setoid functions instances
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Following discussion we had last week I've started to define those
instances and it occurred to me that they would make nice addition to
the base library.

I've removed requirement for `Products (Set q)` instance from lawful
`CartesianClosed`.  It seems it wasn't used anywhere and I didn't know
what that would be here.

Provided instances quantify `Level`s individually as they're different
for different typeclasses.  Quantifiyng that at the module level would
mean that we wouldn't be able to substitute it differently.  For
example: `Products` can use `Setoid c ℓ` as `obj`.  But
`Exponentials` require that `obj` is `Setoid (c ⊔ ℓ) (c ⊔ ℓ)`, which
in turns requires `Products` for the same `obj`.  Fixing `c` and `ℓ`
at the module would prohibit `Exponentials` to get required
`Products`.

One module (`Function.Construct.Setoid`) was copied from
agda-categories, and there it was copied from old standard library, as
it got removed from the 2.0 version.
---
 src/Felix/All.agda                   |   1 +
 src/Felix/Instances/Setoid.agda      |   5 ++
 src/Felix/Instances/Setoid/Laws.agda |  48 ++++++++++++
 src/Felix/Instances/Setoid/Raw.agda  | 106 +++++++++++++++++++++++++++
 src/Felix/Instances/Setoid/Type.agda |  57 ++++++++++++++
 src/Felix/Laws.agda                  |   2 +-
 src/Function/Construct/Setoid.agda   |  31 ++++++++
 7 files changed, 249 insertions(+), 1 deletion(-)
 create mode 100644 src/Felix/Instances/Setoid.agda
 create mode 100644 src/Felix/Instances/Setoid/Laws.agda
 create mode 100644 src/Felix/Instances/Setoid/Raw.agda
 create mode 100644 src/Felix/Instances/Setoid/Type.agda
 create mode 100644 src/Function/Construct/Setoid.agda

diff --git a/src/Felix/All.agda b/src/Felix/All.agda
index bfabf06..cadae96 100644
--- a/src/Felix/All.agda
+++ b/src/Felix/All.agda
@@ -22,3 +22,4 @@ import Felix.Construct.Arrow
 import Felix.Instances.Function
 import Felix.Instances.Function.Lift
 import Felix.Instances.Identity
+import Felix.Instances.Setoid
diff --git a/src/Felix/Instances/Setoid.agda b/src/Felix/Instances/Setoid.agda
new file mode 100644
index 0000000..f198ff9
--- /dev/null
+++ b/src/Felix/Instances/Setoid.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid where
+
+open import Felix.Instances.Setoid.Laws public
diff --git a/src/Felix/Instances/Setoid/Laws.agda b/src/Felix/Instances/Setoid/Laws.agda
new file mode 100644
index 0000000..f3df26b
--- /dev/null
+++ b/src/Felix/Instances/Setoid/Laws.agda
@@ -0,0 +1,48 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid.Laws where
+
+open import Data.Product using (_,_)
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (mk⇔)
+open import Level using (_⊔_)
+open import Relation.Binary using (Setoid)
+
+open import Felix.Equiv using (Equivalent)
+open import Felix.Raw hiding (Category; Cartesian; CartesianClosed)
+open import Felix.Laws using (Category; Cartesian; CartesianClosed)
+
+open import Felix.Instances.Setoid.Raw public
+
+module setoid-laws-instances where instance
+
+  category : ∀ {c ℓ} → Category {obj = Setoid c ℓ} _⟶_
+  category = record
+    { identityˡ = λ {_} {B} _ → Setoid.refl B
+    ; identityʳ = λ {_} {B} _ → Setoid.refl B
+    ; assoc = λ {_} {_} {_} {D} _ → Setoid.refl D
+    ; ∘≈ = λ { {_} {_} {C} {f = f} {k = k} h≈k f≈g x →
+      Setoid.trans C (h≈k (f ⟨$⟩ x)) (cong k (f≈g x)) }
+    }
+
+  cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
+  cartesian {c} {ℓ} = record
+    { ∀⊤ = λ _ → tt
+    ; ∀× = λ {A} {B} {C} {f} {g} {k} → mk⇔
+      (λ k≈f▵g → (λ x → cong (exl {a = B} {b = C}) (k≈f▵g x))
+               , (λ x → cong (exr {a = B} {b = C}) (k≈f▵g x)))
+      (λ (exl∘k≈f , exr∘k≈g) x → exl∘k≈f x , exr∘k≈g x)
+    ; ▵≈ = λ h≈k f≈g x → h≈k x , f≈g x
+    }
+
+  cartesianClosed :
+    ∀ {c ℓ} →
+    CartesianClosed
+      ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
+      ⦃ raw = setoid-raw-instances.cartesianClosed {c} {ℓ} ⦄
+  cartesianClosed = record
+    { ∀⇛ = λ {_} {_} {C} → mk⇔
+      (λ g≈curry-f (a , b) → Setoid.sym C (g≈curry-f a {b}))
+      (λ f≈uncurry-g a → λ {b} → Setoid.sym C (f≈uncurry-g (a , b)))
+    ; curry≈ = λ f≈g a → λ {b} → f≈g (a , b)
+    }
diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
new file mode 100644
index 0000000..6adb5e8
--- /dev/null
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -0,0 +1,106 @@
+{-# OPTIONS --safe --without-K  #-}
+
+module Felix.Instances.Setoid.Raw where
+
+open import Data.Product using (_,_; <_,_>; proj₁; proj₂; uncurry′; ∃₂)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Sum using ([_,_]; inj₁; inj₂)
+open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂)
+open import Data.Unit.Polymorphic using (tt) renaming (⊤ to ⊤′)
+open import Function using (Congruent; Func; _∘′_; flip′) renaming (_∘_ to _∘ᵈ_)
+open import Function.Construct.Composition as Comp
+open import Function.Construct.Constant as Const
+open import Function.Construct.Identity as Id
+open import Function.Construct.Setoid as Fun
+open import Level using (_⊔_; suc)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using ()
+
+open import Felix.Equiv using (Equivalent)
+open import Felix.Raw
+  using ( Category; _∘_
+        ; Cartesian; exl; _⊗_; constʳ
+        ; Cocartesian; CartesianClosed; Traced
+        ; ⊤; _×_
+        )
+open import Felix.Instances.Setoid.Type using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
+open setoid-instances public
+
+module setoid-raw-instances where instance
+
+  category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_
+  category = record
+    { id = Id.function _
+    ; _∘_ = flip′ Comp.function
+    }
+
+  cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
+  cartesian = record
+    { ! = Const.function _ ⊤ tt
+    ; _▵_ = λ ac ad → record
+      { to = < ac ⟨$⟩_ , ad ⟨$⟩_ >
+      ; cong = < cong ac , cong ad >
+      }
+    ; exl = record
+      { to = proj₁
+      ; cong = proj₁
+      }
+    ; exr = record
+      { to = proj₂
+      ; cong = proj₂
+      }
+    }
+
+  cocartesian : ∀ {c ℓ} → Cocartesian ⦃ coproducts {c} {ℓ} ⦄ _⟶_
+  cocartesian {c} {ℓ} = record
+    { ¡ = record
+      { to = λ { () }
+      ; cong = λ { {()} }
+      }
+    ; _▿_ = λ ac bc → record
+      { to = [ ac ⟨$⟩_ , bc ⟨$⟩_ ]
+      ; cong = λ where
+        (inj₁ x) → cong ac x
+        (inj₂ x) → cong bc x
+      }
+    ; inl = record
+      { to = inj₁
+      ; cong = inj₁
+      }
+    ; inr = record
+      { to = inj₂
+      ; cong = inj₂
+      }
+    }
+
+  cartesianClosed :
+    ∀ {c ℓ} →
+    CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
+  cartesianClosed = record
+    { curry = λ {A} {B} f → record
+      { to = λ a → record
+        { to = λ b → f ⟨$⟩ (a , b)
+        ; cong = λ x≈y → cong f (Setoid.refl A , x≈y)
+        }
+      ; cong = λ x≈y → cong f (x≈y , Setoid.refl B)
+      }
+    ; apply = λ {A} {B} → record
+      { to = uncurry′ _⟨$⟩_
+      ; cong = λ { {f , x} {g , y} (f≈g , x≈y) →
+        Setoid.trans B (f≈g {x}) (cong g x≈y) }
+      }
+    }
+
+  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
+  equivalent = record
+    { _≈_ = λ {From} {To} f g →
+      let open Setoid To
+      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
+    ; equiv = λ {From} {To} →
+      let open Setoid To
+       in record
+         { refl = λ _ → refl
+         ; sym = λ f≈g x → sym (f≈g x)
+         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+         }
+    }
diff --git a/src/Felix/Instances/Setoid/Type.agda b/src/Felix/Instances/Setoid/Type.agda
new file mode 100644
index 0000000..247559f
--- /dev/null
+++ b/src/Felix/Instances/Setoid/Type.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Felix.Instances.Setoid.Type where
+
+open import Data.Empty.Polymorphic renaming (⊥ to ⊥′)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Data.Sum.Relation.Binary.Pointwise using (⊎-setoid)
+open import Data.Unit.Polymorphic renaming (⊤ to ⊤′)
+open import Function using (Func)
+open import Function.Construct.Setoid renaming (setoid to ⟶-setoid)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Setoid)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+infixr 0 _⟶_
+_⟶_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+_⟶_ = Func
+
+open Func using (cong) public
+
+infixl 5 _⟨$⟩_
+_⟨$⟩_ : ∀ {c ℓ} → ∀ {A B : Setoid c ℓ} →
+  A ⟶ B → Setoid.Carrier A → Setoid.Carrier B
+_⟨$⟩_ = Func.to
+
+module setoid-instances {c ℓ} where
+  open import Felix.Object using (Coproducts; Exponentials; Products)
+
+  instance
+    products : Products (Setoid c ℓ)
+    products = record
+      { ⊤ = record
+        { Carrier = ⊤′
+        ; _≈_ = λ _ _ → ⊤′
+        }
+      ; _×_ = ×-setoid
+      }
+
+    coproducts : Coproducts (Setoid c (c ⊔ ℓ))
+    coproducts = record
+      { ⊥ = record
+        { Carrier = ⊥′
+        ; _≈_ = λ { () () }
+        ; isEquivalence = record
+          { refl = λ { {()} }
+          ; sym = λ { {()} {()} _ }
+          ; trans = λ { {()} {()} {()} _ _ }
+          }
+        }
+      ; _⊎_ = ⊎-setoid
+      }
+
+    exponentials : Exponentials (Setoid (c ⊔ ℓ) (c ⊔ ℓ))
+    exponentials = record { _⇛_ = ⟶-setoid }
diff --git a/src/Felix/Laws.agda b/src/Felix/Laws.agda
index 7565942..499f4d9 100644
--- a/src/Felix/Laws.agda
+++ b/src/Felix/Laws.agda
@@ -291,7 +291,7 @@ record CartesianClosed {obj : Set o} ⦃ _ : Products obj ⦄
                        {q} ⦃ _ : Equivalent q _⇨′_ ⦄
                        ⦃ _ : R.Category _⇨′_ ⦄
                        ⦃ _ : R.Cartesian _⇨′_ ⦄
-                       ⦃ _ : R.CartesianClosed _⇨′_ ⦄
+                       ⦃ raw : R.CartesianClosed _⇨′_ ⦄
                        ⦃ lCat : Category _⇨′_ ⦄ ⦃ lCart : Cartesian _⇨′_ ⦄
        : Set (o ⊔ ℓ ⊔ q) where
   private infix 0 _⇨_; _⇨_ = _⇨′_
diff --git a/src/Function/Construct/Setoid.agda b/src/Function/Construct/Setoid.agda
new file mode 100644
index 0000000..b877bd7
--- /dev/null
+++ b/src/Function/Construct/Setoid.agda
@@ -0,0 +1,31 @@
+-- agda-categories says that it:
+-- was not ported from old function hierarchy
+
+{-# OPTIONS --without-K --safe #-}
+
+-- was not ported from old function hierarchy
+
+module Function.Construct.Setoid where
+
+  open import Function.Bundles using (Func)
+  import Function.Construct.Composition as Comp
+  open import Level using (Level)
+  open import Relation.Binary.Bundles using (Setoid)
+
+
+  private
+    variable
+      a₁ a₂ b₁ b₂ c₁ c₂ : Level
+
+  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+  setoid From To = record
+    { Carrier = Func From To
+    ; _≈_ = λ f g → ∀ {x} → Func.to f x To.≈ Func.to g x
+    ; isEquivalence = record
+      { refl = To.refl
+      ; sym = λ f≈g → To.sym f≈g
+      ; trans = λ f≈g g≈h → To.trans f≈g g≈h
+      }
+    }
+    where
+      module To = Setoid To

From df2cf2fec1c95947b422230e7ba8bf870206a355 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Thu, 8 Feb 2024 09:31:29 +0100
Subject: [PATCH 3/8] Use more standard library

---
 src/Felix/Instances/Setoid/Raw.agda | 41 ++++++++---------------------
 1 file changed, 11 insertions(+), 30 deletions(-)

diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
index 6adb5e8..0831515 100644
--- a/src/Felix/Instances/Setoid/Raw.agda
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -2,10 +2,11 @@
 
 module Felix.Instances.Setoid.Raw where
 
-open import Data.Product using (_,_; <_,_>; proj₁; proj₂; uncurry′; ∃₂)
+open import Data.Product using (_,_; curry′; uncurry′; ∃₂)
+open import Data.Product.Function.NonDependent.Setoid using (<_,_>ₛ; proj₁ₛ; proj₂ₛ)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum using ([_,_]; inj₁; inj₂)
-open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂)
+open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
 open import Data.Unit.Polymorphic using (tt) renaming (⊤ to ⊤′)
 open import Function using (Congruent; Func; _∘′_; flip′) renaming (_∘_ to _∘ᵈ_)
 open import Function.Construct.Composition as Comp
@@ -37,18 +38,9 @@ module setoid-raw-instances where instance
   cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
   cartesian = record
     { ! = Const.function _ ⊤ tt
-    ; _▵_ = λ ac ad → record
-      { to = < ac ⟨$⟩_ , ad ⟨$⟩_ >
-      ; cong = < cong ac , cong ad >
-      }
-    ; exl = record
-      { to = proj₁
-      ; cong = proj₁
-      }
-    ; exr = record
-      { to = proj₂
-      ; cong = proj₂
-      }
+    ; _▵_ = <_,_>ₛ
+    ; exl = proj₁ₛ
+    ; exr = proj₂ₛ
     }
 
   cocartesian : ∀ {c ℓ} → Cocartesian ⦃ coproducts {c} {ℓ} ⦄ _⟶_
@@ -57,20 +49,9 @@ module setoid-raw-instances where instance
       { to = λ { () }
       ; cong = λ { {()} }
       }
-    ; _▿_ = λ ac bc → record
-      { to = [ ac ⟨$⟩_ , bc ⟨$⟩_ ]
-      ; cong = λ where
-        (inj₁ x) → cong ac x
-        (inj₂ x) → cong bc x
-      }
-    ; inl = record
-      { to = inj₁
-      ; cong = inj₁
-      }
-    ; inr = record
-      { to = inj₂
-      ; cong = inj₂
-      }
+    ; _▿_ = [_,_]ₛ
+    ; inl = inj₁ₛ
+    ; inr = inj₂ₛ
     }
 
   cartesianClosed :
@@ -79,8 +60,8 @@ module setoid-raw-instances where instance
   cartesianClosed = record
     { curry = λ {A} {B} f → record
       { to = λ a → record
-        { to = λ b → f ⟨$⟩ (a , b)
-        ; cong = λ x≈y → cong f (Setoid.refl A , x≈y)
+        { to = curry′ (f ⟨$⟩_) a
+        ; cong = curry′ (cong f) (Setoid.refl A)
         }
       ; cong = λ x≈y → cong f (x≈y , Setoid.refl B)
       }

From 85c1856f5ba9db7c954a022e8941554905cdd45f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Fri, 9 Feb 2024 12:37:45 +0100
Subject: [PATCH 4/8] Use more standard categorical operators
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Actually I don't use that much _categorical operators_, as I couldn't
get proper categorical instances to work.  That is, Setoid categorical
laws are functions in the category of (Agda) function and types.
However I couldn't figure out the Level of Set that I should set to
`Felix.Instance.Function` in order to use those operators in laws
definitions.  So I settled for next best thing and used standard
library provided functions.  And oh boy, did I got surprised by the
results. Taking for example the `▵≈` law from the `Cartesian`. It
holds by `<_,_>` (which is the definition of _▵_ in category of
functions and types)!

This has completely stunned me. Law for the categorical operator holds
by the definition of this operator in different category!  I find it
amazing!

The same holds for `curry` in the `CartesianClosed`,  *but* I couldn't
figure it out for `∘≈` in the `Category`.  I wonder why?

I wonder if this has something to do with the fact that there is
trivial homomorphism from the category of `Setoid`s to category of
function and types via `⟦_⟧ = Func.to`?

In order to make `CartesianClosed` simplification to work I needed to
make argument to `Setoid` of setoid functions explicit.
Unfortunately in the upcoming PR it is implicit.
---
 src/Felix/Instances/Setoid/Laws.agda | 25 +++++++++++++++----------
 src/Felix/Instances/Setoid/Raw.agda  |  9 +++++----
 src/Function/Construct/Setoid.agda   |  8 ++++----
 3 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/src/Felix/Instances/Setoid/Laws.agda b/src/Felix/Instances/Setoid/Laws.agda
index f3df26b..c36f334 100644
--- a/src/Felix/Instances/Setoid/Laws.agda
+++ b/src/Felix/Instances/Setoid/Laws.agda
@@ -2,14 +2,15 @@
 
 module Felix.Instances.Setoid.Laws where
 
-open import Data.Product using (_,_)
+open import Data.Product using (_,_; <_,_>; curry; uncurry)
 open import Data.Unit.Polymorphic using (tt)
-open import Function using (mk⇔)
+open import Function using (_∘_; _∘₂_; mk⇔)
 open import Level using (_⊔_)
 open import Relation.Binary using (Setoid)
 
 open import Felix.Equiv using (Equivalent)
-open import Felix.Raw hiding (Category; Cartesian; CartesianClosed)
+open import Felix.Raw as Raw
+  hiding (Category; Cartesian; CartesianClosed; _∘_; curry; uncurry)
 open import Felix.Laws using (Category; Cartesian; CartesianClosed)
 
 open import Felix.Instances.Setoid.Raw public
@@ -27,12 +28,16 @@ module setoid-laws-instances where instance
 
   cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
   cartesian {c} {ℓ} = record
+    -- ! in category of function and types
     { ∀⊤ = λ _ → tt
     ; ∀× = λ {A} {B} {C} {f} {g} {k} → mk⇔
-      (λ k≈f▵g → (λ x → cong (exl {a = B} {b = C}) (k≈f▵g x))
-               , (λ x → cong (exr {a = B} {b = C}) (k≈f▵g x)))
-      (λ (exl∘k≈f , exr∘k≈g) x → exl∘k≈f x , exr∘k≈g x)
-    ; ▵≈ = λ h≈k f≈g x → h≈k x , f≈g x
+      < cong (exl {a = B} {b = C}) ∘_
+      , cong (exr {a = B} {b = C}) ∘_
+      >
+      (uncurry <_,_>)
+    -- this is _▵_ in category of functions and types,
+    -- but I have trouble hinting to agda what Level it should use
+    ; ▵≈ = <_,_>
     }
 
   cartesianClosed :
@@ -42,7 +47,7 @@ module setoid-laws-instances where instance
       ⦃ raw = setoid-raw-instances.cartesianClosed {c} {ℓ} ⦄
   cartesianClosed = record
     { ∀⇛ = λ {_} {_} {C} → mk⇔
-      (λ g≈curry-f (a , b) → Setoid.sym C (g≈curry-f a {b}))
-      (λ f≈uncurry-g a → λ {b} → Setoid.sym C (f≈uncurry-g (a , b)))
-    ; curry≈ = λ f≈g a → λ {b} → f≈g (a , b)
+      (λ g≈curry-f → Setoid.sym C ∘ uncurry g≈curry-f)
+      (λ f≈uncurry-g → Setoid.sym C ∘₂ curry f≈uncurry-g)
+    ; curry≈ = curry
     }
diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
index 0831515..f90eed5 100644
--- a/src/Felix/Instances/Setoid/Raw.agda
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -8,7 +8,7 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum using ([_,_]; inj₁; inj₂)
 open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
 open import Data.Unit.Polymorphic using (tt) renaming (⊤ to ⊤′)
-open import Function using (Congruent; Func; _∘′_; flip′) renaming (_∘_ to _∘ᵈ_)
+open import Function using (Congruent; Func; _∘′_) renaming (_∘_ to _∘ᵈ_)
 open import Function.Construct.Composition as Comp
 open import Function.Construct.Constant as Const
 open import Function.Construct.Identity as Id
@@ -32,7 +32,8 @@ module setoid-raw-instances where instance
   category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_
   category = record
     { id = Id.function _
-    ; _∘_ = flip′ Comp.function
+    -- flip′ Comp.function doesn't reduce in goals
+    ; _∘_ = λ g f → Comp.function f g
     }
 
   cartesian : ∀ {c ℓ} → Cartesian {obj = Setoid c ℓ} _⟶_
@@ -63,12 +64,12 @@ module setoid-raw-instances where instance
         { to = curry′ (f ⟨$⟩_) a
         ; cong = curry′ (cong f) (Setoid.refl A)
         }
-      ; cong = λ x≈y → cong f (x≈y , Setoid.refl B)
+      ; cong = λ x≈y _ → cong f (x≈y , Setoid.refl B)
       }
     ; apply = λ {A} {B} → record
       { to = uncurry′ _⟨$⟩_
       ; cong = λ { {f , x} {g , y} (f≈g , x≈y) →
-        Setoid.trans B (f≈g {x}) (cong g x≈y) }
+        Setoid.trans B (f≈g x) (cong g x≈y) }
       }
     }
 
diff --git a/src/Function/Construct/Setoid.agda b/src/Function/Construct/Setoid.agda
index b877bd7..8049990 100644
--- a/src/Function/Construct/Setoid.agda
+++ b/src/Function/Construct/Setoid.agda
@@ -20,11 +20,11 @@ module Function.Construct.Setoid where
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
   setoid From To = record
     { Carrier = Func From To
-    ; _≈_ = λ f g → ∀ {x} → Func.to f x To.≈ Func.to g x
+    ; _≈_ = λ f g → ∀ x → Func.to f x To.≈ Func.to g x
     ; isEquivalence = record
-      { refl = To.refl
-      ; sym = λ f≈g → To.sym f≈g
-      ; trans = λ f≈g g≈h → To.trans f≈g g≈h
+      { refl = λ _ → To.refl
+      ; sym = λ f≈g x → To.sym (f≈g x)
+      ; trans = λ f≈g g≈h x → To.trans (f≈g x) (g≈h x)
       }
     }
     where

From 1aae1cbc7de8aa324fba0f9e6e18634b58be45b3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Mon, 5 Feb 2024 15:16:45 +0100
Subject: [PATCH 5/8] Some Traced instance for setoid functions

By using categorical operations I don't have to come up with `cong`
proof manually.  It will be composed instead.
I don't know however if this definition is good one, so it'll be
commented out for the time being.
---
 src/Felix/Instances/Setoid/Raw.agda | 55 +++++++++++++++--------------
 1 file changed, 29 insertions(+), 26 deletions(-)

diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
index f90eed5..663e4d2 100644
--- a/src/Felix/Instances/Setoid/Raw.agda
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -2,33 +2,40 @@
 
 module Felix.Instances.Setoid.Raw where
 
-open import Data.Product using (_,_; curry′; uncurry′; ∃₂)
+open import Data.Product using (_,_; _,′_; curry′; uncurry′; ∃₂; proj₁; proj₂)
 open import Data.Product.Function.NonDependent.Setoid using (<_,_>ₛ; proj₁ₛ; proj₂ₛ)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum using ([_,_]; inj₁; inj₂)
 open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
-open import Data.Unit.Polymorphic using (tt) renaming (⊤ to ⊤′)
-open import Function using (Congruent; Func; _∘′_) renaming (_∘_ to _∘ᵈ_)
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (Func) renaming (_∘_ to _∘ᵈ_)
 open import Function.Construct.Composition as Comp
 open import Function.Construct.Constant as Const
 open import Function.Construct.Identity as Id
-open import Function.Construct.Setoid as Fun
 open import Level using (_⊔_; suc)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using ()
 
 open import Felix.Equiv using (Equivalent)
 open import Felix.Raw
-  using ( Category; _∘_
-        ; Cartesian; exl; _⊗_; constʳ
-        ; Cocartesian; CartesianClosed; Traced
-        ; ⊤; _×_
-        )
-open import Felix.Instances.Setoid.Type using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
+open import Felix.Instances.Setoid.Type
+  using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
 open setoid-instances public
 
 module setoid-raw-instances where instance
 
+  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
+  equivalent = record
+    { _≈_ = λ {From} {To} f g →
+      let open Setoid To
+      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
+    ; equiv = λ {From} {To} →
+      let open Setoid To
+       in record
+         { refl = λ _ → refl
+         ; sym = λ f≈g x → sym (f≈g x)
+         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+         }
+    }
+
   category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_
   category = record
     { id = Id.function _
@@ -55,6 +62,16 @@ module setoid-raw-instances where instance
     ; inr = inj₂ₛ
     }
 
+  -- omit until I can be sure it's ok
+  -- traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
+  -- traced = record
+  --   { WF = λ {_} {s} {b} f →
+  --     let open Equivalent equivalent in
+  --     ∃₂ λ (y : ⊤ ⟶ b) (z : ⊤ ⟶ s) →
+  --     f ∘ constʳ z ≈ (y ⦂ z) ∘ !
+  --   ; trace = λ { f (y , z , eq) → exl ∘ f ∘ constʳ z }
+  --   }
+
   cartesianClosed :
     ∀ {c ℓ} →
     CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
@@ -72,17 +89,3 @@ module setoid-raw-instances where instance
         Setoid.trans B (f≈g x) (cong g x≈y) }
       }
     }
-
-  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
-  equivalent = record
-    { _≈_ = λ {From} {To} f g →
-      let open Setoid To
-      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
-    ; equiv = λ {From} {To} →
-      let open Setoid To
-       in record
-         { refl = λ _ → refl
-         ; sym = λ f≈g x → sym (f≈g x)
-         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
-         }
-    }

From c15cb16c8bbb416e0c667cebb0b9a327319ff091 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Tue, 20 Feb 2024 16:23:43 +0100
Subject: [PATCH 6/8] Remove duplicated comment

---
 src/Function/Construct/Setoid.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Function/Construct/Setoid.agda b/src/Function/Construct/Setoid.agda
index 8049990..a11d6d4 100644
--- a/src/Function/Construct/Setoid.agda
+++ b/src/Function/Construct/Setoid.agda
@@ -1,10 +1,9 @@
 -- agda-categories says that it:
--- was not ported from old function hierarchy
+-- was not ported from old function hierarchy, see:
+-- https://github.com/agda/agda-stdlib/pull/2240
 
 {-# OPTIONS --without-K --safe #-}
 
--- was not ported from old function hierarchy
-
 module Function.Construct.Setoid where
 
   open import Function.Bundles using (Func)

From ddfb20af4d5ad0a0640b92f88586c3039c490e7b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Tue, 20 Feb 2024 21:02:11 +0100
Subject: [PATCH 7/8] Reuse function setoid for equivalent instance

---
 src/Felix/Instances/Setoid/Raw.agda | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
index 663e4d2..2d80691 100644
--- a/src/Felix/Instances/Setoid/Raw.agda
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -14,6 +14,7 @@ open import Function.Construct.Identity as Id
 open import Level using (_⊔_; suc)
 open import Relation.Binary using (Setoid)
 
+open import Function.Construct.Setoid using (setoid)
 open import Felix.Equiv using (Equivalent)
 open import Felix.Raw
 open import Felix.Instances.Setoid.Type
@@ -24,16 +25,8 @@ module setoid-raw-instances where instance
 
   equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
   equivalent = record
-    { _≈_ = λ {From} {To} f g →
-      let open Setoid To
-      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
-    ; equiv = λ {From} {To} →
-      let open Setoid To
-       in record
-         { refl = λ _ → refl
-         ; sym = λ f≈g x → sym (f≈g x)
-         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
-         }
+    { _≈_ = λ {From} {To} → Setoid._≈_ (setoid From To)
+    ; equiv = λ {From} {To} → Setoid.isEquivalence (setoid From To)
     }
 
   category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_

From 6a0a811dac3c8852599133b1a468721ebbd5039b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= <jakub@famisoft.pl>
Date: Thu, 22 Feb 2024 10:28:02 +0100
Subject: [PATCH 8/8] Setoids distributive instance

---
 src/Felix/Instances/Setoid/Laws.agda | 30 +++++++++++++++++++++++++---
 src/Felix/Instances/Setoid/Raw.agda  | 29 +++++++++++++++++++++++++--
 src/Felix/Laws.agda                  |  2 +-
 3 files changed, 55 insertions(+), 6 deletions(-)

diff --git a/src/Felix/Instances/Setoid/Laws.agda b/src/Felix/Instances/Setoid/Laws.agda
index c36f334..b351c9d 100644
--- a/src/Felix/Instances/Setoid/Laws.agda
+++ b/src/Felix/Instances/Setoid/Laws.agda
@@ -3,6 +3,9 @@
 module Felix.Instances.Setoid.Laws where
 
 open import Data.Product using (_,_; <_,_>; curry; uncurry)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Relation.Binary.Pointwise using (_⊎ₛ_)
 open import Data.Unit.Polymorphic using (tt)
 open import Function using (_∘_; _∘₂_; mk⇔)
 open import Level using (_⊔_)
@@ -10,8 +13,8 @@ open import Relation.Binary using (Setoid)
 
 open import Felix.Equiv using (Equivalent)
 open import Felix.Raw as Raw
-  hiding (Category; Cartesian; CartesianClosed; _∘_; curry; uncurry)
-open import Felix.Laws using (Category; Cartesian; CartesianClosed)
+  hiding (Category; Cartesian; CartesianClosed; Distributive; _∘_; curry; uncurry)
+open import Felix.Laws using (Category; Cartesian; CartesianClosed; Distributive)
 
 open import Felix.Instances.Setoid.Raw public
 
@@ -30,7 +33,7 @@ module setoid-laws-instances where instance
   cartesian {c} {ℓ} = record
     -- ! in category of function and types
     { ∀⊤ = λ _ → tt
-    ; ∀× = λ {A} {B} {C} {f} {g} {k} → mk⇔
+    ; ∀× = λ {A} {B} {C} → mk⇔
       < cong (exl {a = B} {b = C}) ∘_
       , cong (exr {a = B} {b = C}) ∘_
       >
@@ -40,6 +43,27 @@ module setoid-laws-instances where instance
     ; ▵≈ = <_,_>
     }
 
+  distributive :
+    ∀ {c ℓ} →
+    Distributive
+      ⦃ products {c} {c ⊔ ℓ} ⦄ ⦃ coproducts {c} {ℓ} ⦄
+      _⟶_
+      ⦃ raw = setoid-raw-instances.distributive {c} {ℓ} ⦄
+  distributive = record
+    { distribˡ∘distribˡ⁻¹ = λ where
+      {A} {B} {C} (_ , inj₁ _) → Setoid.refl (A ×ₛ (B ⊎ₛ C))
+      {A} {B} {C} (_ , inj₂ _) → Setoid.refl (A ×ₛ (B ⊎ₛ C))
+    ; distribˡ⁻¹∘distribˡ = λ where
+      {A} {B} {C} (inj₁ _) → Setoid.refl ((A ×ₛ B) ⊎ₛ (A ×ₛ C))
+      {A} {B} {C} (inj₂ _) → Setoid.refl ((A ×ₛ B) ⊎ₛ (A ×ₛ C))
+    ; distribʳ∘distribʳ⁻¹ = λ where
+      {A} {B} {C} (inj₁ _ , _) → Setoid.refl ((B ⊎ₛ C) ×ₛ A)
+      {A} {B} {C} (inj₂ _ , _) → Setoid.refl ((B ⊎ₛ C) ×ₛ A)
+    ; distribʳ⁻¹∘distribʳ = λ where
+      {A} {B} {C} (inj₁ _) → Setoid.refl ((B ×ₛ A) ⊎ₛ (C ×ₛ A))
+      {A} {B} {C} (inj₂ _) → Setoid.refl ((B ×ₛ A) ⊎ₛ (C ×ₛ A))
+    }
+
   cartesianClosed :
     ∀ {c ℓ} →
     CartesianClosed
diff --git a/src/Felix/Instances/Setoid/Raw.agda b/src/Felix/Instances/Setoid/Raw.agda
index 2d80691..b370dc5 100644
--- a/src/Felix/Instances/Setoid/Raw.agda
+++ b/src/Felix/Instances/Setoid/Raw.agda
@@ -6,6 +6,7 @@ open import Data.Product using (_,_; _,′_; curry′; uncurry′; ∃₂; proj
 open import Data.Product.Function.NonDependent.Setoid using (<_,_>ₛ; proj₁ₛ; proj₂ₛ)
 open import Data.Sum using ([_,_]; inj₁; inj₂)
 open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
+open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂)
 open import Data.Unit.Polymorphic using (tt)
 open import Function using (Func) renaming (_∘_ to _∘ᵈ_)
 open import Function.Construct.Composition as Comp
@@ -19,6 +20,9 @@ open import Felix.Equiv using (Equivalent)
 open import Felix.Raw
 open import Felix.Instances.Setoid.Type
   using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
+
+import Felix.Instances.Function as Fun
+
 open setoid-instances public
 
 module setoid-raw-instances where instance
@@ -29,7 +33,7 @@ module setoid-raw-instances where instance
     ; equiv = λ {From} {To} → Setoid.isEquivalence (setoid From To)
     }
 
-  category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_
+  category : ∀ {c ℓ} → Category {obj = Setoid c ℓ} _⟶_
   category = record
     { id = Id.function _
     -- flip′ Comp.function doesn't reduce in goals
@@ -45,7 +49,7 @@ module setoid-raw-instances where instance
     }
 
   cocartesian : ∀ {c ℓ} → Cocartesian ⦃ coproducts {c} {ℓ} ⦄ _⟶_
-  cocartesian {c} {ℓ} = record
+  cocartesian = record
     { ¡ = record
       { to = λ { () }
       ; cong = λ { {()} }
@@ -55,6 +59,27 @@ module setoid-raw-instances where instance
     ; inr = inj₂ₛ
     }
 
+  distributive :
+    ∀ {c ℓ} →
+    Distributive
+      ⦃ products {c} {c ⊔ ℓ} ⦄ ⦃ coproducts {c} {ℓ} ⦄
+      _⟶_
+      ⦃ category {c} {c ⊔ ℓ} ⦄ ⦃ cartesian {c} {c ⊔ ℓ} ⦄ ⦃ cocartesian {c} {ℓ} ⦄
+  distributive {c} {ℓ} = let open Fun c in record
+    { distribˡ⁻¹ = record
+      { to = distribˡ⁻¹
+      ; cong = λ where
+        (a₁≈a₂ , inj₁ b₁≈b₂) → inj₁ (a₁≈a₂ , b₁≈b₂)
+        (a₁≈a₂ , inj₂ c₁≈c₂) → inj₂ (a₁≈a₂ , c₁≈c₂)
+      }
+    ; distribʳ⁻¹ = record
+      { to = distribʳ⁻¹
+      ; cong = λ where
+        (inj₁ b₁≈b₂ , a₁≈a₂) → inj₁ (b₁≈b₂ , a₁≈a₂)
+        (inj₂ c₁≈c₂ , a₁≈a₂) → inj₂ (c₁≈c₂ , a₁≈a₂)
+      }
+    }
+
   -- omit until I can be sure it's ok
   -- traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
   -- traced = record
diff --git a/src/Felix/Laws.agda b/src/Felix/Laws.agda
index 499f4d9..c8d4a25 100644
--- a/src/Felix/Laws.agda
+++ b/src/Felix/Laws.agda
@@ -274,7 +274,7 @@ record Distributive
   (_⇨′_ : obj → obj → Set ℓ)
   {q} ⦃ _ : Equivalent q _⇨′_ ⦄
   ⦃ _ : R.Category _⇨′_ ⦄ ⦃ _ : R.Cartesian _⇨′_ ⦄ ⦃ _ : R.Cocartesian _⇨′_ ⦄
-  ⦃ _ : R.Distributive _⇨′_ ⦄
+  ⦃ raw : R.Distributive _⇨′_ ⦄
   ⦃ _ : Category _⇨′_ ⦄ ⦃ _ : Cartesian _⇨′_ ⦄
     : Set (o ⊔ ℓ ⊔ q) where
   field