Use more standard categorical operators

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

@@ -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
     }

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 = λ b → to f (a , b)
         ; cong = λ x≈y → cong f (Setoid.refl A , x≈y)
         }
-      ; 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′ to
       ; 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) }
       }
     }
 

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