From 6d6ca43329145cd9bf624c0e1877a5c77d3c6bfc Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Mon, 12 Aug 2024 15:28:00 -0700
Subject: [PATCH] chore: fix separators

---
 .../Diagram/Coequaliser/RegularEpi.lagda.md   |  2 +-
 src/Cat/Diagram/Separator.lagda.md            | 28 +++++++++----------
 src/Cat/Diagram/Separator/Regular.lagda.md    |  2 +-
 3 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md b/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md
index 7ce995624..abdb4d027 100644
--- a/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md
+++ b/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md
@@ -210,7 +210,7 @@ follows by yet more brute-force calculation.
       (∐F.universal _ _ C.∘ ∐Ob.match F.₀ ∐F.ψ) C.∘ ∐Ob.ι F.₀ j ≡⟨ C.pullr (∐Ob.commute _) ⟩
       ∐F.universal _ _ C.∘ ∐F.ψ j                               ≡⟨ ∐F.factors _ _ ⟩
       e' C.∘ ∐Ob.ι F.₀ j                                        ∎
-  indexed-coproduct→regular-epi .has-is-coeq .unique {e' = e'} {colim = h} p =
+  indexed-coproduct→regular-epi .has-is-coeq .unique {e' = e'} {other = h} p =
     ∐F.unique _ _ _ λ j →
       h C.∘ ∐F.ψ j                               ≡˘⟨ ap₂ C._∘_ refl (∐Ob.commute _) ⟩
       h C.∘ (∐Ob.match F.₀ ∐F.ψ C.∘ ∐Ob.ι F.₀ j) ≡⟨ C.pulll p ⟩
diff --git a/src/Cat/Diagram/Separator.lagda.md b/src/Cat/Diagram/Separator.lagda.md
index 2679bae93..19d8c61e0 100644
--- a/src/Cat/Diagram/Separator.lagda.md
+++ b/src/Cat/Diagram/Separator.lagda.md
@@ -264,7 +264,7 @@ $S$ is a separating family.
 ```agda
 equalisers+conservative→separator
   : ∀ {s}
-  → has-equalisers C
+  → Equalisers C
   → is-conservative (Hom-from C s)
   → is-separator s
 ```
@@ -276,9 +276,9 @@ $e$ being an equaliser.
 
 ```agda
 equalisers+conservative→separator equalisers f∘-conservative {f = f} {g = g} p =
-  invertible→epic equ-invertible f g Eq.equal
+  invertible→epic equ-invertible f g equal
   where
-    module Eq = Equaliser (equalisers f g)
+    open Equalisers equalisers
 ```
 
 Moreover, $\cC(S,-)$ is conservative, so it suffices to prove that
@@ -286,14 +286,14 @@ precomposition of $e$ with an $S$-generalized element is an equivalence.
 This follows immediately from the universal property of equalisers!
 
 ```agda
-    equ-invertible : is-invertible Eq.equ
+    equ-invertible : is-invertible (equ f g)
     equ-invertible =
       f∘-conservative $
       is-equiv→is-invertible $
       is-iso→is-equiv $ iso
-        (λ e → Eq.universal (p e))
-        (λ e → Eq.factors)
-        (λ h → sym (Eq.unique refl))
+        (λ e → equalise e (p e))
+        (λ e → equ∘equalise)
+        (λ h → sym (equalise-unique refl))
 ```
 
 A similar line of argument lets us generalize this result to separating
@@ -302,7 +302,7 @@ families.
 ```agda
 equalisers+jointly-conservative→separating-family
   : ∀ {κ} {Idx : Type κ} {sᵢ : Idx → Ob}
-  → has-equalisers C
+  → Equalisers C
   → is-jointly-conservative (λ i → Hom-from C (sᵢ i))
   → is-separating-family sᵢ
 ```
@@ -313,18 +313,18 @@ equalisers+jointly-conservative→separating-family
 ```agda
 equalisers+jointly-conservative→separating-family
   equalisers fᵢ∘-conservative {f = f} {g = g} p =
-  invertible→epic equ-invertible f g Eq.equal
+  invertible→epic equ-invertible f g equal
   where
-    module Eq = Equaliser (equalisers f g)
+    open Equalisers equalisers
 
-    equ-invertible : is-invertible Eq.equ
+    equ-invertible : is-invertible (equ f g)
     equ-invertible =
       fᵢ∘-conservative λ i →
       is-equiv→is-invertible $
       is-iso→is-equiv $ iso
-        (λ eᵢ → Eq.universal (p eᵢ))
-        (λ eᵢ → Eq.factors)
-        (λ h → sym (Eq.unique refl))
+        (λ eᵢ → equalise eᵢ (p eᵢ))
+        (λ eᵢ → equ∘equalise)
+        (λ h → sym (equalise-unique refl))
 ```
 </details>
 
diff --git a/src/Cat/Diagram/Separator/Regular.lagda.md b/src/Cat/Diagram/Separator/Regular.lagda.md
index 2c0df6d0f..503305db0 100644
--- a/src/Cat/Diagram/Separator/Regular.lagda.md
+++ b/src/Cat/Diagram/Separator/Regular.lagda.md
@@ -135,7 +135,7 @@ This is straightforward enough to prove with sufficient elbow grease.
       (dense.universal _ ∘ ⊗!.match _ _ _) ∘ ⊗!.ι _ _ e ≡⟨ pullr (⊗!.commute _ _) ⟩
       dense.universal _ ∘ e                             ≡⟨ dense.commute ⟩
       e' ∘ ⊗!.ι _ _ e                                   ∎
-  regular .has-is-coeq .unique {e' = e'} {colim = h} p =
+  regular .has-is-coeq .unique {e' = e'} {other = h} p =
     dense.unique _ λ e →
       h ∘ e                           ≡˘⟨ ap (h ∘_) (⊗!.commute (Hom s x) s) ⟩
       h ∘ ⊗!.match _ _ _ ∘ ⊗!.ι _ _ e ≡⟨ pulll p ⟩