Revert "change definition of function sets equality to not build-in c…

…ong (see agda-stdlib issue #1467 for further information). Fix everything that needed fixed because of that - a lot."

This reverts commit c0b2661.

This is because this shouldn't have been done on master, but through a branch
(which it now is) and will get a proper review.

src/Categories/Adjoint.agda

@@ -185,18 +185,18 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve
           { to = λ f → lift (Ladjunct (lower f))
           ; cong = λ eq → lift (Ladjunct-resp-≈ (lower eq))
           }
-        ; commute = λ _ → lift $ Ladjunct-comm D.Equiv.refl
+        ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq)
         }
       ; F⇐G = ntHelper record
         { η       = λ _ → record
           { to = λ f → lift (Radjunct (lower f))
           ; cong = λ eq → lift (Radjunct-resp-≈ (lower eq))
           }
-        ; commute = λ _ → lift $ Radjunct-comm C.Equiv.refl
+        ; commute = λ _ eq → lift $ Radjunct-comm (lower eq)
         }
       ; iso = λ X → record
-        { isoˡ = lift RLadjunct≈id
-        ; isoʳ = lift LRadjunct≈id
+        { isoˡ = λ eq → let open D.HomReasoning in lift (RLadjunct≈id ○ lower eq)
+        ; isoʳ = λ eq → let open C.HomReasoning in lift (LRadjunct≈id ○ lower eq)
         }
       }
 

src/Categories/Adjoint/Equivalents.agda

@@ -50,15 +50,15 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
     Hom-NI′ = record
       { F⇒G = ntHelper record
         { η       = λ _ → record { to = Hom-inverse.to ; cong = Hom-inverse.to-cong }
-        ; commute = λ _ → Ladjunct-comm D.Equiv.refl
+        ; commute = λ _ eq → Ladjunct-comm eq
         }
       ; F⇐G = ntHelper record
         { η       = λ _ → record { to = Hom-inverse.from ; cong = Hom-inverse.from-cong }
-        ; commute = λ _ → Radjunct-comm C.Equiv.refl
+        ; commute = λ _ eq → Radjunct-comm eq
         }
       ; iso = λ _ → record
-        { isoˡ = RLadjunct≈id
-        ; isoʳ = LRadjunct≈id
+        { isoˡ = λ eq → let open D.HomReasoning in RLadjunct≈id ○ eq
+        ; isoʳ = λ eq → let open C.HomReasoning in LRadjunct≈id ○ eq
         }
       }
 
@@ -88,10 +88,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
         { η       = λ X → unitη X ⟨$⟩ D.id
         ; commute = λ {X} {Y} f → begin
           (unitη Y ⟨$⟩ D.id) ∘ f                             ≈⟨ introˡ R.identity ⟩
-          R.F₁ D.id ∘ (unitη Y  ⟨$⟩ D.id) ∘ f                ≈˘⟨ ⇒.commute (f , D.id) ⟩
+          R.F₁ D.id ∘ (unitη Y  ⟨$⟩ D.id) ∘ f                ≈˘⟨ ⇒.commute (f , D.id) D.Equiv.refl ⟩
           ⇒.η (X , L.F₀ Y) ⟨$⟩ (D.id D.∘ D.id D.∘ L.F₁ f)    ≈⟨ cong (⇒.η (X , L.F₀ Y)) (D.Equiv.trans D.identityˡ D.identityˡ) ⟩
           ⇒.η (X , L.F₀ Y) ⟨$⟩ L.F₁ f                        ≈⟨ cong (⇒.η (X , L.F₀ Y)) (MR.introʳ D (MR.elimʳ D L.identity)) ⟩
-          ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) ⟩
+          ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) D.Equiv.refl ⟩
           R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id) ∘ id            ≈⟨ refl⟩∘⟨ identityʳ ⟩
           R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id)                 ∎
         }
@@ -107,10 +107,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
         { η       = λ X → counitη X ⟨$⟩ C.id
         ; commute = λ {X} {Y} f → begin
           (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)               ≈˘⟨ identityˡ ⟩
-          id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)          ≈˘⟨ ⇐.commute (R.F₁ f , D.id) ⟩
+          id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)          ≈˘⟨ ⇐.commute (R.F₁ f , D.id) C.Equiv.refl ⟩
           ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ R.F₁ f) ≈⟨ cong (⇐.η (R.F₀ X , Y)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
           ⇐.η (R.F₀ X , Y) ⟨$⟩ R.F₁ f                        ≈⟨ cong (⇐.η (R.F₀ X , Y)) (MR.introʳ C C.identityˡ) ⟩
-          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id)    ≈⟨ ⇐.commute (C.id , f) ⟩
+          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id)    ≈⟨ ⇐.commute (C.id , f) C.Equiv.refl ⟩
           f ∘ (counitη X ⟨$⟩ C.id) ∘ L.F₁ C.id               ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
           f ∘ (counitη X ⟨$⟩ C.id)                           ∎
         }
@@ -129,10 +129,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
             open MR D
         in begin
           η counit (L.F₀ A) ∘ L.F₁ (η unit A)      ≈˘⟨ identityˡ ⟩
-          id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) ⟩
+          id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) C.Equiv.refl ⟩
           ⇐.η (A , L.F₀ A) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ η unit A)
                                                    ≈⟨ cong (⇐.η (A , L.F₀ A)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
-          ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A            ≈⟨ isoˡ ⟩
+          ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A            ≈⟨ isoˡ refl ⟩
           id
                                                    ∎
       ; zag    = λ {B} →
@@ -142,10 +142,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
             open MR C
         in begin
           R.F₁ (η counit B) ∘ η unit (R.F₀ B)      ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
-          R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) ⟩
+          R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) D.Equiv.refl ⟩
           ⇒.η (R.F₀ B , B) ⟨$⟩ (η counit B D.∘ D.id D.∘ L.F₁ id)
                                                    ≈⟨ cong (⇒.η (R.F₀ B , B)) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
-          ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B          ≈⟨ isoʳ ⟩
+          ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B          ≈⟨ isoʳ refl ⟩
           id                                       ∎
       }
       where module i {X} = Iso (iso X)
@@ -180,13 +180,13 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
           lower (unitη Y ⟨$⟩ lift D.id) ∘ f
             ≈⟨ introˡ R.identity ⟩
           R.F₁ D.id ∘ lower (unitη Y ⟨$⟩ lift D.id) ∘ f
-            ≈˘⟨ lower (⇒.commute (f , D.id)) ⟩
+            ≈˘⟨ lower (⇒.commute (f , D.id) (lift D.Equiv.refl)) ⟩
           lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (D.id D.∘ D.id D.∘ L.F₁ f))
             ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (D.Equiv.trans D.identityˡ D.identityˡ))) ⟩
           lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f))
             ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (MR.introʳ D (MR.elimʳ D L.identity)))) ⟩
           lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f D.∘ D.id D.∘ L.F₁ id))
-            ≈⟨ lower (⇒.commute (C.id , L.F₁ f)) ⟩
+            ≈⟨ lower (⇒.commute (C.id , L.F₁ f) (lift D.Equiv.refl)) ⟩
           R.F₁ (L.F₁ f) ∘ lower (⇒.η (X , L.F₀ X) ⟨$⟩ lift D.id) ∘ id
             ≈⟨ refl⟩∘⟨ identityʳ ⟩
           F₁ (R ∘F L) f ∘ lower (unitη X ⟨$⟩ lift D.id)                ∎
@@ -205,13 +205,13 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
           lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
             ≈˘⟨ identityˡ ⟩
           id ∘ lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
-            ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id)) ⟩
+            ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id) (lift C.Equiv.refl)) ⟩
           lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ R.F₁ f))
             ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
           lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f))
             ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (MR.introʳ C C.identityˡ))) ⟩
           lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f C.∘ C.id C.∘ C.id))
-            ≈⟨ lower (⇐.commute (C.id , f)) ⟩
+            ≈⟨ lower (⇐.commute (C.id , f) (lift C.Equiv.refl)) ⟩
           f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id) ∘ L.F₁ C.id
             ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
           f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id)
@@ -234,11 +234,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
           lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
             ≈˘⟨ identityˡ ⟩
           id ∘ lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
-            ≈˘⟨ lower (⇐.commute (η unit A , id)) ⟩
+            ≈˘⟨ lower (⇐.commute (η unit A , id) (lift C.Equiv.refl)) ⟩
           lower (⇐.η (A , L.F₀ A) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ lower (⇒.η (A , L.F₀ A) ⟨$⟩ lift id)))
             ≈⟨ lower (cong (⇐.η (A , L.F₀ A)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
           lower (⇐.η (A , L.F₀ A) ⟨$⟩ (⇒.η (A , L.F₀ A) ⟨$⟩ lift id))
-            ≈⟨ lower (isoˡ) ⟩
+            ≈⟨ lower (isoˡ (lift refl)) ⟩
           id ∎
       ; zag    = λ {B} →
         let open C
@@ -249,11 +249,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
           R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id)
             ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
           R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id) ∘ id
-            ≈˘⟨ lower (⇒.commute (id , η counit B)) ⟩
+            ≈˘⟨ lower (⇒.commute (id , η counit B) (lift D.Equiv.refl)) ⟩
           lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id) D.∘ D.id D.∘ L.F₁ id))
             ≈⟨ lower (cong (⇒.η (R.F₀ B , B)) (lift (MR.elimʳ D (MR.elimʳ D L.identity)))) ⟩
           lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)))
-            ≈⟨ lower isoʳ ⟩
+            ≈⟨ lower (isoʳ (lift refl)) ⟩
           id ∎
       }
       where open NaturalTransformation

src/Categories/Adjoint/Instance/0-Truncation.agda

@@ -5,18 +5,19 @@ module Categories.Adjoint.Instance.0-Truncation where
 -- The adjunction between 0-truncation and the inclusion functor from
 -- Setoids to Categories/Groupoids.
 
+open import Level using (Lift)
+open import Data.Unit using (⊤)
 open import Function.Base renaming (id to id→)
 open import Function.Bundles using (Func)
 import Function.Construct.Identity as Id
 open import Relation.Binary using (Setoid)
 
 open import Categories.Adjoint using (_⊣_)
-open import Categories.Category.Core using (Category)
 open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
 open import Categories.Category.Groupoid using (Groupoid)
 open import Categories.Category.Instance.Groupoids using (Groupoids)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Instance.0-Truncation using (Trunc)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)
@@ -33,8 +34,8 @@ Inclusion {c} {ℓ} e = record
     let module S = Setoid S
         module T = Setoid T
     in record
-    { F⇒G = record { η = λ _ → f≗g       }
-    ; F⇐G = record { η = λ _ → T.sym f≗g }
+    { F⇒G = record { η = λ _ → f≗g S.refl         }
+    ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) }
     }
   }
   where open Func
@@ -45,7 +46,7 @@ TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
 TruncAdj {o} {ℓ} {e} = record
   { unit   = unit
   ; counit = counit
-  ; zig    = λ {A} → Category.id (category A)
+  ; zig    = id→
   ; zag    = refl
   }
   where
@@ -60,4 +61,4 @@ TruncAdj {o} {ℓ} {e} = record
       }
 
     counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
-    counit = ntHelper record { η = Id.function; commute = λ {_} {Y} _ → Setoid.refl Y }
+    counit = ntHelper record { η = Id.function; commute = λ f → cong f }

src/Categories/Adjoint/Instance/PosetCore.agda

@@ -40,7 +40,7 @@ Forgetful = record
   ; F₁           = λ f → mkPosetHomo _ _ (to f) (cong f)
   ; identity     = λ {S}       → refl S
   ; homomorphism = λ {_ _ S}   → refl S
-  ; F-resp-≈     = λ {S _} f≗g → f≗g
+  ; F-resp-≈     = λ {S _} f≗g → f≗g (refl S)
   }
   where
     Forgetful₀ : ∀ {c ℓ} → Setoid c ℓ → Poset c ℓ ℓ
@@ -72,20 +72,20 @@ Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ
 Core = record
   { F₀           = λ A → record { isEquivalence = isEquivalence A }
   ; F₁           = λ f → record { to = ⟦ f ⟧ ; cong = cong f }
-  ; identity     = λ {A} → Eq.refl A
-  ; homomorphism = λ {_ _ Z} → Eq.refl Z
-  ; F-resp-≈     = λ f≗g → f≗g
+  ; identity     = Function.id
+  ; homomorphism = λ {_ _ _ f g} → cong (Comp.posetHomomorphism f g)
+  ; F-resp-≈     = λ {_ B} {f _} f≗g x≈y → Eq.trans B (cong f x≈y) f≗g
   }
   where open Poset
 
 -- Core is right-adjoint to the forgetful functor
 
 CoreAdj : ∀ {o ℓ} → Forgetful ⊣ Core {o} {ℓ} {ℓ}
 CoreAdj = record
-  { unit   = ntHelper record { η = unit   ; commute = λ {_} {Y} _ → Setoid.refl Y}
+  { unit   = ntHelper record { η = unit   ; commute = cong                  }
   ; counit = ntHelper record { η = counit ; commute = λ {_ B} _ → Eq.refl B }
   ; zig    = λ {S} → Setoid.refl S
-  ; zag    = λ {B} → Eq.refl B
+  ; zag    = Function.id
   }
   where
     open Poset

src/Categories/Adjoint/Mate.agda

@@ -8,7 +8,7 @@ open import Level
 open import Data.Product using (Σ; _,_)
 open import Function.Bundles using (Func; _⟨$⟩_)
 open import Function.Construct.Composition using (function)
-open import Function.Construct.Setoid using () renaming (setoid to _⇨_)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
 open import Relation.Binary using (Setoid; IsEquivalence)
 
 open import Categories.Category
@@ -135,13 +135,13 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
 
     mate-commute₁ : function D⟶C (F₁ Hom[ C ][-,-] (C.id , β.η Y))
                   ≈ function (F₁ Hom[ D ][-,-] (α.η X , D.id)) D⟶C′
-    mate-commute₁ {f} = begin
+    mate-commute₁ {f} {g} f≈g = begin
       β.η Y ∘ (F₁ R′ f ∘ L′⊣R′.unit.η X) ∘ C.id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
       β.η Y ∘ F₁ R′ f ∘ L′⊣R′.unit.η X           ≈⟨ pullˡ (β.commute f) ⟩
       (F₁ R f ∘ β.η (F₀ L′ X)) ∘ L′⊣R′.unit.η X  ≈˘⟨ pushʳ commute₁ ⟩
       F₁ R f ∘ F₁ R (α.η X) ∘ L⊣R.unit.η X       ≈˘⟨ pushˡ (homomorphism R) ⟩
-      F₁ R (f D.∘ α.η X) ∘ L⊣R.unit.η X          ≈⟨ F-resp-≈ R (DH.⟺ D.identityˡ) ⟩∘⟨refl ⟩
-      F₁ R (D.id D.∘ f D.∘ α.η X) ∘ L⊣R.unit.η X ∎
+      F₁ R (f D.∘ α.η X) ∘ L⊣R.unit.η X          ≈⟨ F-resp-≈ R (D.∘-resp-≈ˡ f≈g DH.○ DH.⟺ D.identityˡ) ⟩∘⟨refl ⟩
+      F₁ R (D.id D.∘ g D.∘ α.η X) ∘ L⊣R.unit.η X ∎
 
   module _ {X : C.Obj} {Y : D.Obj} where
     open D hiding (_≈_)
@@ -173,13 +173,13 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
 
     mate-commute₂ : function C⟶D (F₁ Hom[ D ][-,-] (α.η X , D.id))
                   ≈ function (F₁ Hom[ C ][-,-] (C.id , β.η Y)) C⟶D′
-    mate-commute₂ {f} = begin
+    mate-commute₂ {f} {g} f≈g = begin
       D.id ∘ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X  ≈⟨ identityˡ ⟩
       (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X         ≈˘⟨ pushʳ (α.commute f) ⟩
       L′⊣R′.counit.η Y ∘ α.η (F₀ R′ Y) ∘ F₁ L f    ≈˘⟨ pushˡ commute₂ ⟩
       (L⊣R.counit.η Y ∘ F₁ L (β.η Y)) ∘ F₁ L f     ≈˘⟨ pushʳ (homomorphism L) ⟩
-      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f)          ≈⟨ refl⟩∘⟨ F-resp-≈ L (C.∘-resp-≈ʳ (CH.⟺ C.identityʳ)) ⟩
-      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f C.∘ C.id) ∎
+      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f)          ≈⟨ refl⟩∘⟨ F-resp-≈ L (C.∘-resp-≈ʳ (f≈g CH.○ CH.⟺ C.identityʳ)) ⟩
+      L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ g C.∘ C.id) ∎
 
 -- alternatively, if commute₃ and commute₄ are shown, then a Mate can be constructed.