wip: crunch through a couple of files

src/Algebra/Group/Cat/FinitelyComplete.lagda.md

@@ -157,6 +157,8 @@ inj₂ {H} {G} .monic g h x = Grp↪Sets-is-faithful (funext λ e i → (x i # e
 
 ```agda
 open import Cat.Diagram.Equaliser
+
+open Equalisers
 ```
 
 The equaliser of two group homomorphisms $f, g : G \to H$ is given by
@@ -166,18 +168,12 @@ in sets, and re-use all of its infrastructure to make an equaliser in
 `Groups`{.Agda}.
 
 ```agda
-module _ {G H : Group ℓ} (f g : Groups.Hom G H) where
-  private
-    module G = Group-on (G .snd)
-    module H = Group-on (H .snd)
-
-    module f = is-group-hom (f .preserves)
-    module g = is-group-hom (g .preserves)
-    module seq = Equaliser
-      (SL.Sets-equalisers
-        {A = G.underlying-set}
-        {B = H.underlying-set}
-        (f .hom) (g .hom))
+Groups-equalisers : Equalisers (Groups ℓ)
+Groups-equalisers .Eq {G} {H} f g = to-group equ-group where
+  module G = Group-on (G .snd)
+  module H = Group-on (H .snd)
+  module f = is-group-hom (f .preserves)
+  module g = is-group-hom (g .preserves)
 ```
 
 Recall that points there are elements of the domain (here, a point $x :
@@ -187,60 +183,45 @@ structure from $G$ to $\rm{equ}(f,g)$, we must prove that, if $f(x)
 follows from $f$ and $g$ being group homomorphisms:
 
 ```agda
-  Equaliser-group : Group ℓ
-  Equaliser-group = to-group equ-group where
-    equ-⋆ : ∣ seq.apex ∣ → ∣ seq.apex ∣ → ∣ seq.apex ∣
-    equ-⋆ (a , p) (b , q) = (a G.⋆ b) , r where abstract
-      r : f # (G .snd ._⋆_ a b) ≡ g # (G .snd ._⋆_ a b)
-      r = f.pres-⋆ a b ·· ap₂ H._⋆_ p q ·· sym (g.pres-⋆ _ _)
-
-    equ-inv : ∣ seq.apex ∣ → ∣ seq.apex ∣
-    equ-inv (x , p) = x G.⁻¹ , q where abstract
-      q : f # (G.inverse x) ≡ g # (G.inverse x)
-      q = f.pres-inv ·· ap H._⁻¹ p ·· sym g.pres-inv
-
-    abstract
-      invs : f # G.unit ≡ g # G.unit
-      invs = f.pres-id ∙ sym g.pres-id
+  equ-group : make-group (Σ[ x ∈ G ] (f # x ≡ g # x))
+  equ-group .make-group.group-is-set = hlevel 2
+  equ-group .make-group.mul (x , p) (y , q) =
+    x G.⋆ y , ⋆-eq where abstract
+      ⋆-eq : f # (x G.⋆ y) ≡ g # (x G.⋆ y)
+      ⋆-eq = f.pres-⋆ _ _ ·· ap₂ H._⋆_ p q ·· sym (g.pres-⋆ _ _)
 ```
 
 Similar yoga must be done for the inverse maps and the group unit.
 
 ```agda
-    equ-group : make-group ∣ seq.apex ∣
-    equ-group .make-group.group-is-set = seq.apex .is-tr
-    equ-group .make-group.unit = G.unit , invs
-    equ-group .make-group.mul = equ-⋆
-    equ-group .make-group.inv = equ-inv
-    equ-group .make-group.assoc x y z = Σ-prop-path! G.associative
-    equ-group .make-group.invl x = Σ-prop-path! G.inversel
-    equ-group .make-group.idl x = Σ-prop-path! G.idl
-
-  open is-equaliser
-  open Equaliser
+  equ-group .make-group.unit =
+    G.unit , unit-eq where abstract
+      unit-eq : f # G.unit ≡ g # G.unit
+      unit-eq = f.pres-id ∙ sym g.pres-id
+  equ-group .make-group.inv (x , p) =
+    x G.⁻¹ , inv-eq where abstract
+      inv-eq : f # (G.inverse x) ≡ g # (G.inverse x)
+      inv-eq = f.pres-inv ·· ap H._⁻¹ p ·· sym g.pres-inv
+  equ-group .make-group.assoc x y z = Σ-prop-path! G.associative
+  equ-group .make-group.invl x = Σ-prop-path! G.inversel
+  equ-group .make-group.idl x = Σ-prop-path! G.idl
 ```
 
-We can then, pretty effortlessly, prove that the
-`Equaliser-group`{.Agda}, together with the canonical injection
-$\rm{equ}(f,g) \mono G$, equalise the group homomorphisms $f$ and
-$g$.
-
-```agda
-  Groups-equalisers : Equaliser (Groups ℓ) f g
-  Groups-equalisers .apex = Equaliser-group
-  Groups-equalisers .equ = total-hom fst record { pres-⋆ = λ x y → refl }
-  Groups-equalisers .has-is-eq .equal = Grp↪Sets-is-faithful seq.equal
-  Groups-equalisers .has-is-eq .universal {F = F} {e'} p = total-hom go lim-gh where
-    go = seq.universal {F = underlying-set (F .snd)} (ap hom p)
+We can then, pretty effortlessly, prove that this group, together with
+the canonical injection $\rm{equ}(f,g) \mono G$, equalise the group
+homomorphisms $f$ and $g$.
 
-    lim-gh : is-group-hom _ _ go
-    lim-gh .pres-⋆ x y = Σ-prop-path! (e' .preserves .pres-⋆ _ _)
 
-  Groups-equalisers .has-is-eq .factors {F = F} {p = p} = Grp↪Sets-is-faithful
-    (seq.factors {F = underlying-set (F .snd)} {p = ap hom p})
-
-  Groups-equalisers .has-is-eq .unique {F = F} {p = p} q = Grp↪Sets-is-faithful
-    (seq.unique {F = underlying-set (F .snd)} {p = ap hom p} (ap hom q))
+```agda
+Groups-equalisers .equ f g .hom = fst
+Groups-equalisers .equ f g .preserves .pres-⋆ _ _ = refl
+Groups-equalisers .equal = ext (λ x p → p)
+Groups-equalisers .equalise e p .hom x = e # x , p #ₚ x
+Groups-equalisers .equalise e p .preserves .pres-⋆ x y =
+  Σ-prop-path! (e .preserves .pres-⋆ x y)
+Groups-equalisers .equ∘equalise = trivial!
+Groups-equalisers .equalise-unique p =
+  ext λ x → Σ-prop-path! (p #ₚ x)
 ```
 
 Putting all of these constructions together, we get the proof that

src/Cat/Diagram/Equaliser.lagda.md

@@ -184,21 +184,21 @@ record Equalisers {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
     Eq : ∀ {X Y} → Hom X Y → Hom X Y → Ob
     equ : ∀ {X Y} → (f g : Hom X Y) → Hom (Eq f g) X
     equal : ∀ {X Y} {f g : Hom X Y} → f ∘ equ f g ≡ g ∘ equ f g
-    equate
+    equalise
       : ∀ {E X Y} {f g : Hom X Y}
       → (e : Hom E X)
       → f ∘ e ≡ g ∘ e
       → Hom E (Eq f g)
-    equ∘equate
+    equ∘equalise
       : ∀ {E X Y} {f g : Hom X Y}
       → {e : Hom E X} {p : f ∘ e ≡ g ∘ e}
-      → equ f g ∘ equate e p ≡ e
-    equate-unique
+      → equ f g ∘ equalise e p ≡ e
+    equalise-unique
       : ∀ {E X Y} {f g : Hom X Y}
       → {e : Hom E X} {p : f ∘ e ≡ g ∘ e}
       → {other : Hom E (Eq f g)}
       → equ f g ∘ other ≡ e
-      → other ≡ equate e p
+      → other ≡ equalise e p
 ```
 
 <!--
@@ -207,9 +207,9 @@ record Equalisers {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
   equaliser f g .Equaliser.apex = Eq f g
   equaliser f g .Equaliser.equ = equ f g
   equaliser f g .Equaliser.has-is-eq .is-equaliser.equal = equal
-  equaliser f g .Equaliser.has-is-eq .is-equaliser.universal = equate _
-  equaliser f g .Equaliser.has-is-eq .is-equaliser.factors = equ∘equate
-  equaliser f g .Equaliser.has-is-eq .is-equaliser.unique = equate-unique
+  equaliser f g .Equaliser.has-is-eq .is-equaliser.universal = equalise _
+  equaliser f g .Equaliser.has-is-eq .is-equaliser.factors = equ∘equalise
+  equaliser f g .Equaliser.has-is-eq .is-equaliser.unique = equalise-unique
 
   private module equaliser {X Y} {f g : Hom X Y} = Equaliser (equaliser f g)
   open equaliser
@@ -231,8 +231,8 @@ to-equalisers {C = C} has-equalisers = equalisers where
   equalisers .Eq f g = eq.apex {f = f} {g = g}
   equalisers .equ _ _ = eq.equ
   equalisers .equal = eq.equal
-  equalisers .equate _ = eq.universal
-  equalisers .equ∘equate = eq.factors
-  equalisers .equate-unique = eq.unique
+  equalisers .equalise _ = eq.universal
+  equalisers .equ∘equalise = eq.factors
+  equalisers .equalise-unique = eq.unique
 ```
 -->

src/Cat/Diagram/Equaliser/Kernel.lagda.md

@@ -38,15 +38,15 @@ $f$.
 ```agda
   module _ (∅ : Zero C) where
     open Zero ∅
-  
+
     is-kernel : ∀ {a b ker} (f : Hom a b) (k : Hom ker a) → Type _
     is-kernel f = is-equaliser C f zero→
-  
+
     kernels-are-subobjects
       : ∀ {a b ker} {f : Hom a b} (k : Hom ker a)
       → is-kernel f k → is-monic k
     kernels-are-subobjects = is-equaliser→is-monic
-  
+
     record Kernel {a b} (f : Hom a b) : Type (o ⊔ ℓ) where
       field
         {ker} : Ob
@@ -62,14 +62,16 @@ pair of morphisms, then it has canonically-defined choices of kernels:
 
 ```agda
   module Canonical-kernels
-    (zero : Zero C) (eqs : ∀ {a b} (f g : Hom a b) → Equaliser C f g) where
+    (zero : Zero C)
+    (equalisers : Equalisers C) where
     open Zero zero
+    open Equalisers equalisers
     open Kernel
-  
+
     Ker : ∀ {a b} (f : Hom a b) → Kernel zero f
     Ker f .ker           = _
-    Ker f .kernel        = eqs f zero→ .Equaliser.equ
-    Ker f .has-is-kernel = eqs _ _ .Equaliser.has-is-eq
+    Ker f .kernel        = equ f zero→
+    Ker f .has-is-kernel = has-is-eq
 ```
 
 We now show that the maps $! : \ker\ker f \to \emptyset$ and $¡ :

src/Cat/Diagram/Limit/Base.lagda.md

@@ -880,7 +880,7 @@ as the data for a limit.
       Cod .π (a , b , f) C.∘ ⌜ s C.∘ equ s t ⌝ ≡⟨ ap! equal ⟩
       Cod .π (a , b , f) C.∘ t C.∘ equ s t     ≡⟨ C.pulll (Cod .commute) ⟩
       Obs .π b C.∘ equ  s t                    ∎
-    lim .universal {x} e comm = equate e' comm' where
+    lim .universal {x} e comm = equalise e' comm' where
       e' : C.Hom x (Obs .ΠF)
       e' = Obs .tuple e
       comm' : s C.∘ e' ≡ t C.∘ e'
@@ -892,10 +892,10 @@ as the data for a limit.
         Obs .π b C.∘ e'              ≡˘⟨ C.pulll (Cod .commute) ⟩
         Cod .π i C.∘ t C.∘ e'        ∎
     lim .factors {j} e comm =
-      (Obs .π j C.∘ equ s t) C.∘ lim .universal e comm ≡⟨ C.pullr equ∘equate ⟩
+      (Obs .π j C.∘ equ s t) C.∘ lim .universal e comm ≡⟨ C.pullr equ∘equalise ⟩
       Obs .π j C.∘ Obs .tuple e                        ≡⟨ Obs .commute ⟩
       e j                                              ∎
-    lim .unique e comm u' fac = equate-unique $ Obs .unique _
+    lim .unique e comm u' fac = equalise-unique $ Obs .unique _
       λ i → C.assoc _ _ _ ∙ fac i
 ```
 </details>

src/Cat/Displayed/Instances/Subobjects.lagda.md

@@ -121,7 +121,6 @@ open Cartesian-fibration
 open is-weak-cocartesian
 open Cartesian-lift
 open is-cartesian
-open Pullback
 ```
 -->
 
@@ -160,24 +159,25 @@ is enough for its uniqueness.
 
 ```agda
 Subobject-fibration
-  : has-pullbacks B
+  : Pullbacks B
   → Cartesian-fibration Subobjects
-Subobject-fibration pb .has-lift f y' = l where
-  it : Pullback _ _ _
-  it = pb (y' .map) f
+Subobject-fibration pullbacks .has-lift f y' = l where
+  open Pullbacks pullbacks
+
   l : Cartesian-lift Subobjects f y'
 
   -- The blue square:
-  l .x' .domain = it .apex
-  l .x' .map    = it .p₂
-  l .x' .monic  = is-monic→pullback-is-monic (y' .monic) (it .has-is-pb)
-  l .lifting .map = it .p₁
-  l .lifting .sq  = sym (it .square)
+  l .x' .domain = Pb (y' .map) f
+  l .x' .map    = p₂ (y' .map) f
+  l .x' .monic  = is-monic→pullback-is-monic (y' .monic) has-is-pb
+  -- (it .has-is-pb)
+  l .lifting .map = p₁ (y' .map) f
+  l .lifting .sq  = sym square
 
   -- The dashed red arrow:
   l .cartesian .universal {u' = u'} m h' = λ where
-    .map → it .Pullback.universal (sym (h' .sq) ∙ sym (assoc f m (u' .map)))
-    .sq  → sym (it .p₂∘universal)
+    .map → pb (h' .map) (m ∘ u' .map) (sym (h' .sq) ∙ sym (assoc f m (u' .map)))
+    .sq  → sym p₂∘pb
   l .cartesian .commutes _ _ = prop!
   l .cartesian .unique _ _   = prop!
 ```
@@ -261,7 +261,7 @@ cocartesian fibration must actually be a full opfibration.
 ```agda
 Subobject-opfibration
   : (∀ {x y} (f : Hom x y) → Image B f)
-  → (pb : has-pullbacks B)
+  → (pb : Pullbacks B)
   → Cocartesian-fibration Subobjects
 Subobject-opfibration images pb = cartesian+weak-opfibration→opfibration _
   (Subobject-fibration pb)
@@ -336,31 +336,28 @@ products, regardless of what $y$ is.
 ```agda
 Sub-products
   : ∀ {y}
-  → has-pullbacks B
+  → Pullbacks B
   → Binary-products (Sub y)
-Sub-products {y} pb a b = prod where
-  it = pb (a .map) (b .map)
-
-  prod : Product (Sub y) a b
-  prod .Product.apex .domain = it .apex
-  prod .Product.apex .map = a .map ∘ it .p₁
-  prod .Product.apex .monic = monic-∘
+Sub-products {y} pullbacks = prods where
+  open Pullbacks pullbacks
+  open Binary-products
+
+  prods : Binary-products (Sub y)
+  (prods ⊗₀ a) b .domain = Pb (a .map) (b .map)
+  (prods ⊗₀ a) b .map = a .map ∘ p₁ (a .map) (b .map)
+  (prods ⊗₀ a) b .monic = monic-∘
     (a .monic)
-    (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb)))
-
-  prod .Product.π₁ .map = it .p₁
-  prod .Product.π₁ .sq  = idl _
-
-  prod .Product.π₂ .map = it .p₂
-  prod .Product.π₂ .sq  = idl _ ∙ it .square
-
-  prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .map =
-    it .Pullback.universal {p₁' = q≤a .map} {p₂' = q≤b .map} (sym (q≤a .sq) ∙ q≤b .sq)
-  prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .sq =
-    idl _ ∙ sym (pullr (it .p₁∘universal) ∙ sym (q≤a .sq) ∙ idl _)
-  prod .Product.has-is-product .is-product.π₁∘⟨⟩ = prop!
-  prod .Product.has-is-product .is-product.π₂∘⟨⟩ = prop!
-  prod .Product.has-is-product .is-product.unique _ _ = prop!
+    (is-monic→pullback-is-monic (b .monic) (rotate-pullback has-is-pb))
+  prods .π₁ .map = p₁ _ _
+  prods .π₁ .sq = idl _
+  prods .π₂ .map = p₂ _ _
+  prods .π₂ .sq = idl _ ∙ square
+  prods .⟨_,_⟩ q≤a q≤b .map = pb (q≤a .map) (q≤b .map) (sym (q≤a .sq) ∙ q≤b .sq)
+  prods .⟨_,_⟩ q≤a q≤b .sq =
+      idl _ ∙ sym (pullr p₁∘pb ∙ sym (q≤a .sq) ∙ idl _)
+  prods .π₁∘⟨⟩ = prop!
+  prods .π₂∘⟨⟩ = prop!
+  prods .⟨⟩-unique _ _ = prop!
 ```
 
 ## Univalence