Sets: use ≗

And several follow ons
agda · Jun 2, 2024 · 9d60d80 · 9d60d80
1 parent 429cd39
commit 9d60d80
Show file tree

Hide file tree

Showing 9 changed files with 48 additions and 49 deletions.
diff --git a/src/Categories/Adjoint/Instance/StrictDiscrete.agda b/src/Categories/Adjoint/Instance/StrictDiscrete.agda
@@ -31,9 +31,9 @@ Forgetful : ∀ {o ℓ e} → Functor (StrictCats o ℓ e) (Sets o)
 Forgetful {o} {ℓ} {e} = record
   { F₀ = Obj
   ; F₁ = F₀
-  ; identity     = refl
-  ; homomorphism = refl
-  ; F-resp-≈     = λ F≡G {X} → eq₀ F≡G X
+  ; identity     = λ _ → refl
+  ; homomorphism = λ _ → refl
+  ; F-resp-≈     = eq₀
   }
   where
     open Category
@@ -67,8 +67,8 @@ Discrete {o} = record
                cong g (cong f p)        ∎
     }
   ; F-resp-≈ = λ {_ _ f g} f≗g → record
-    { eq₀ = λ x → f≗g {x}
-    ; eq₁ = λ {x} {y} p → naturality (λ x → subst (f x ≡_) (f≗g {x}) refl)
+    { eq₀ = f≗g
+    ; eq₁ = λ p → naturality (λ x → subst (f x ≡_) (f≗g x) refl)
     }
   }
   where
@@ -110,7 +110,7 @@ Codiscrete {o} ℓ e = record
   ; identity     = Equiv.refl
   ; homomorphism = Equiv.refl
   ; F-resp-≈     = λ {_ _ f g} f≗g → record
-    { eq₀ = λ x → f≗g {x}
+    { eq₀ = f≗g
     ; eq₁ = λ _ → lift tt
     }
   }
@@ -124,7 +124,7 @@ DiscreteLeftAdj {o} = record
   { unit   = unit
   ; counit = counit
   ; zig    = zig
-  ; zag    = refl
+  ; zag    = λ _ → refl
   }
   where
     module U = Functor Forgetful
@@ -169,7 +169,7 @@ CodiscreteRightAdj : ∀ {o ℓ e} → Forgetful ⊣ Codiscrete {o} ℓ e
 CodiscreteRightAdj {o} {ℓ} {e} = record
   { unit   = unit
   ; counit = counit
-  ; zig    = refl
+  ; zig    = λ _ → refl
   ; zag    = zag
   }
   where

diff --git a/src/Categories/Category/Construction/Elements.agda b/src/Categories/Category/Construction/Elements.agda
@@ -29,8 +29,8 @@ Elements {C = C} F = record
   { Obj       = Σ Obj F₀
   ; _⇒_       = λ { (c , x) (c′ , x′) → Σ (c ⇒ c′) (λ f → F₁ f x ≡ x′)  }
   ; _≈_       = λ p q → proj₁ p ≈ proj₁ q
-  ; id        = id , identity
-  ; _∘_       = λ { (f , Ff≡) (g , Fg≡) → f ∘ g ,  trans homomorphism (trans (cong (F₁ f) Fg≡) Ff≡)}
+  ; id        = id , identity _
+  ; _∘_       = λ { (f , Ff≡) (g , Fg≡) → f ∘ g ,  trans (homomorphism _) (trans (cong (F₁ f) Fg≡) Ff≡)}
   ; assoc     = assoc
   ; sym-assoc = sym-assoc
   ; identityˡ = identityˡ
@@ -50,44 +50,44 @@ El {C = C} = record
   { F₀ = Elements
   ; F₁ = λ A⇒B → record
     { F₀ = map idf (η A⇒B _)
-    ; F₁ = map idf λ {f} eq → trans (sym $ commute A⇒B f) (cong (η A⇒B _) eq)
+    ; F₁ = map idf λ {f} eq → trans (sym $ commute A⇒B f _) (cong (η A⇒B _) eq)
     ; identity = Equiv.refl
     ; homomorphism = Equiv.refl
     ; F-resp-≈ = idf
     }
   ; identity = λ {P} → record
     { F⇒G = record
-      { η           = λ X → id , identity P
+      { η           = λ X → id , identity P _ 
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }
     ; F⇐G = record
-      { η           = λ X → id , identity P
+      { η           = λ X → id , identity P _ 
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }
     ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ } }
   ; homomorphism = λ {X₁} {Y₁} {Z₁} → record
     { F⇒G = record
-      { η           = λ X → id , identity Z₁
+      { η           = λ X → id , identity Z₁ _
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }
     ; F⇐G = record
-      { η           = λ X → id , identity Z₁
+      { η           = λ X → id , identity Z₁ _ 
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }
     ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ }
     }
   ; F-resp-≈ = λ {_} {B₁} f≈g → record
     { F⇒G = record
-      { η           = λ _ → id , trans (identity B₁) f≈g
+      { η           = λ _ → id , trans (identity B₁ _) (f≈g _)
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }
     ; F⇐G = record
-      { η           = λ _ → id , trans (identity B₁) (sym f≈g)
+      { η           = λ _ → id , trans (identity B₁ _) (sym (f≈g _ ))
       ; commute     = λ _ → MR.id-comm-sym C
       ; sym-commute = λ _ → MR.id-comm C
       }

diff --git a/src/Categories/Category/Instance/EmptySet.agda b/src/Categories/Category/Instance/EmptySet.agda
@@ -20,7 +20,7 @@ module _ {o : Level} where
   open Init (Sets o)
 
   EmptySet-⊥ : Initial
-  EmptySet-⊥ = record { ⊥ = Lift o ⊥ ; ⊥-is-initial = record { ! = λ { {A} (lift x) → ⊥-elim x } ; !-unique = λ { f {()} } } }
+  EmptySet-⊥ = record { ⊥ = Lift o ⊥ ; ⊥-is-initial = record { ! = λ { {A} (lift x) → ⊥-elim x } ; !-unique = λ { f () } } }
 
 module _ {c ℓ : Level} where
   open Init (Setoids c ℓ)

diff --git a/src/Categories/Category/Instance/PointedSets.agda b/src/Categories/Category/Instance/PointedSets.agda
@@ -33,7 +33,7 @@ Underlying : {o : Level} → Functor (PointedSets o) (Sets o)
 Underlying = record
   { F₀           = proj₁
   ; F₁           = proj₁
-  ; identity     = refl
-  ; homomorphism = refl
-  ; F-resp-≈     = λ f≈g {x} → f≈g x
+  ; identity     = λ _ → refl
+  ; homomorphism = λ _ → refl
+  ; F-resp-≈     = λ f≈g → f≈g
   }
diff --git a/src/Categories/Category/Instance/Sets.agda b/src/Categories/Category/Instance/Sets.agda
@@ -7,30 +7,29 @@ module Categories.Category.Instance.Sets where
 open import Level
 open import Relation.Binary
 open import Function using (_∘′_) renaming (id to idf)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open import Categories.Category
 
 Sets : ∀ o → Category (suc o) o o
 Sets o = record
   { Obj       = Set o
   ; _⇒_       = λ c d → c → d
-  ; _≈_       = λ f g → ∀ {x} → f x ≡ g x
+  ; _≈_       = _≗_
   ; id        = idf
   ; _∘_       = _∘′_
-  ; assoc     = ≡.refl
-  ; sym-assoc = ≡.refl
-  ; identityˡ = ≡.refl
-  ; identityʳ = ≡.refl
-  ; identity² = ≡.refl
+  ; assoc     = λ _ → ≡.refl
+  ; sym-assoc = λ _ → ≡.refl
+  ; identityˡ = λ _ → ≡.refl
+  ; identityʳ = λ _ → ≡.refl
+  ; identity² = λ _ → ≡.refl
   ; equiv     = record
-    { refl  = ≡.refl
-    ; sym   = λ eq → ≡.sym eq
-    ; trans = λ eq₁ eq₂ → ≡.trans eq₁ eq₂
+    { refl  = λ _ → ≡.refl
+    ; sym   = λ eq x → ≡.sym (eq x)
+    ; trans = λ eq₁ eq₂ x → ≡.trans (eq₁ x) (eq₂ x)
     }
   ; ∘-resp-≈  = resp
   }
   where resp : ∀ {A B C : Set o} {f h : B → C} {g i : A → B} →
-                 ({x : B} → f x ≡ h x) →
-                 ({x : A} → g x ≡ i x) → {x : A} → f (g x) ≡ h (i x)
-        resp {h = h} eq₁ eq₂ = ≡.trans eq₁ (≡.cong h eq₂)
+                 (f ≗ h) → (g ≗ i) → f ∘′ g ≗ h ∘′ i
+        resp {h = h} eq₁ eq₂ x = ≡.trans (eq₁ _) (≡.cong h (eq₂ x))
diff --git a/src/Categories/Category/Instance/SingletonSet.agda b/src/Categories/Category/Instance/SingletonSet.agda
@@ -18,7 +18,7 @@ module _ {o : Level} where
   open Term (Sets o)
 
   SingletonSet-⊤ : Terminal
-  SingletonSet-⊤ = record { ⊤ = ⊤ ; ⊤-is-terminal = record { !-unique = λ _ → refl } }
+  SingletonSet-⊤ = record { ⊤ = ⊤ ; ⊤-is-terminal = record { !-unique = λ _ _ → refl } }
 
 module _ {c ℓ : Level} where
   open Term (Setoids c ℓ)

diff --git a/src/Categories/Category/Monoidal/Instance/Sets.agda b/src/Categories/Category/Monoidal/Instance/Sets.agda
@@ -37,9 +37,9 @@ module Product {o : Level} where
     ; π₁ = proj₁
     ; π₂ = proj₂
     ; ⟨_,_⟩ = <_,_>
-    ; project₁ = refl
-    ; project₂ = refl
-    ; unique = λ p₁ p₂ {x} → sym (cong₂ _,_ (p₁ {x}) (p₂ {x}))
+    ; project₁ = λ _ → refl
+    ; project₂ = λ _ → refl
+    ; unique = λ p₁ p₂ x → sym (cong₂ _,_ (p₁ x) (p₂ x))
     } }
 
   Sets-is : Cartesian
@@ -59,9 +59,9 @@ module Coproduct {o : Level} where
     ; i₁ = inj₁
     ; i₂ = inj₂
     ; [_,_] = [_,_]′
-    ; inject₁ = refl
-    ; inject₂ = refl
-    ; unique = λ { i₁ i₂ {inj₁ x} → sym (i₁ {x}) ; i₁ i₂ {inj₂ y} → sym (i₂ {y})} -- stdlib?
+    ; inject₁ = λ _ → refl
+    ; inject₂ = λ _ → refl
+    ; unique = λ { i₁ i₂ (inj₁ x) → sym (i₁ x) ; i₁ i₂ (inj₂ y) → sym (i₂ y)} -- stdlib?
     } }
 
   Sets-is : Cocartesian

diff --git a/src/Categories/Functor/Instance/Discrete.agda b/src/Categories/Functor/Instance/Discrete.agda
@@ -23,7 +23,7 @@ Discrete {o} = record
    ; F₁ = DiscreteFunctor
    ; identity = DiscreteId
    ; homomorphism = PointwiseHom
-   ; F-resp-≈ = ExtensionalityNI
+   ; F-resp-≈ = λ f≗g → ExtensionalityNI f≗g
    }
    where
      DiscreteFunctor : {A B : Set o} → (A → B) → Cats o o o [ D.Discrete A , D.Discrete B ]
@@ -48,9 +48,9 @@ Discrete {o} = record
        ; iso = λ X → record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
        }
      ExtensionalityNI : {A B : Set o} {g h : A → B} →
-      ({x : A} → g x ≡.≡ h x) → NaturalIsomorphism (DiscreteFunctor g) (DiscreteFunctor h)
+      g ≡.≗ h → NaturalIsomorphism (DiscreteFunctor g) (DiscreteFunctor h)
      ExtensionalityNI g≡h = record
-       { F⇒G = ntHelper record { η = λ X → g≡h {X} ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ g≡h)} }
-       ; F⇐G = ntHelper record { η = λ X → ≡.sym (g≡h {X}) ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ _)} }
-       ; iso = λ X → record { isoˡ = ≡.trans-symʳ g≡h ; isoʳ = ≡.trans-symˡ g≡h }
+       { F⇒G = ntHelper record { η = g≡h ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ (g≡h _))} }
+       ; F⇐G = ntHelper record { η = λ X → ≡.sym (g≡h X) ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ _)} }
+       ; iso = λ X → record { isoˡ = ≡.trans-symʳ (g≡h _) ; isoʳ = ≡.trans-symˡ (g≡h _) }
        }
diff --git a/src/Categories/GlobularSet.agda b/src/Categories/GlobularSet.agda
@@ -26,9 +26,9 @@ Trivial : GlobularSet zero
 Trivial = record
   { F₀ = λ _ → ⊤
   ; F₁ = λ _ x → x
-  ; identity = refl
-  ; homomorphism = refl
-  ; F-resp-≈ = λ _ → refl
+  ; identity = λ _ → refl
+  ; homomorphism = λ _ → refl
+  ; F-resp-≈ = λ _ _ → refl
   }
 
 GlobularObject : Category o ℓ e → Set _