chore: match names with Factorisation

Author: plt-amy

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

@@ -48,17 +48,17 @@ pre-existing classes $M$ and $E$ for $m$ and $e$ to belong to.
   record Splitting {X Y : ⌞ C ⌟} (f : Hom X Y) : Type (o ⊔ ℓ) where
     no-eta-equality
     field
-      {mid} : ⌞ C ⌟
-      map   : Hom X mid
-      out   : Hom mid Y
-      com   : f ≡ out ∘ map
+      {mid}   : ⌞ C ⌟
+      left    : Hom X mid
+      right   : Hom mid Y
+      factors : f ≡ right ∘ left
 ```
 
 <!--
 ```agda
   {-# INLINE Splitting.constructor #-}
 
-  open Splitting public
+  open Splitting
 ```
 -->
 
@@ -104,8 +104,8 @@ both the top and bottom rectangles commute.
 ```agda
     field
       map : Hom (s .mid) (t .mid)
-      sq₀ : t.map ∘ sq .top ≡ map     ∘ s.map
-      sq₁ : t.out ∘ map     ≡ sq .bot ∘ s.out
+      sq₀ : t.left ∘ sq .top ≡ map     ∘ s.left
+      sq₁ : t.right ∘ map    ≡ sq .bot ∘ s.right
 ```
 
 In the literature on factorisation systems, the [[total category]] of
@@ -130,15 +130,16 @@ unquoteDecl H-Level-Interpolant = declare-record-hlevel 2 H-Level-Interpolant (q
 
 module _ {o ℓ} {C : Precategory o ℓ} where
   open Precategory C
+  open Splitting
 
   Interpolant-pathp
     : ∀ {X X' Y Y'} {f : Hom X Y} {g : Hom X' Y'} {sq sq' : Homᵃ C f g} {p : sq ≡ sq'} {s : Splitting C f} {t : Splitting C g}
     → {f : Interpolant C sq s t} {g : Interpolant C sq' s t}
     → f .map ≡ g .map
     → PathP (λ i → Interpolant C (p i) s t) f g
   Interpolant-pathp p i .map = p i
-  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₀ = is-prop→pathp (λ i → Hom-set _ _ (t .map ∘ q i .top) (p i ∘ s .map)) (f .sq₀) (g .sq₀) i
-  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₁ = is-prop→pathp (λ i → Hom-set _ _ (t .out ∘ p i) (q i .bot ∘ s .out)) (f .sq₁) (g .sq₁) i
+  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₀ = is-prop→pathp (λ i → Hom-set _ _ (t .left ∘ q i .top) (p i ∘ s .left)) (f .sq₀) (g .sq₀) i
+  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₁ = is-prop→pathp (λ i → Hom-set _ _ (t .right ∘ p i) (q i .bot ∘ s .right)) (f .sq₁) (g .sq₁) i
 
   instance
     Extensional-Interpolant
@@ -214,7 +215,7 @@ module Factorisation {o ℓ} {C : Precategory o ℓ} (fac : Factorisation C) whe
 
   module _ {X Y : ⌞ C ⌟} (f : Hom X Y) where
     open Splitting (Section.S₀ fac (X , Y , f))
-      renaming (mid to Mid ; map to λ→ ; out to ρ→ ; com to factors)
+      renaming (mid to Mid ; left to λ→ ; right to ρ→)
       public
 
   module _ {u v w x : ⌞ C ⌟} {f : Hom u v} {g : Hom w x} (sq : Homᵃ C f g) where

src/Cat/Monoidal/Instances/Factorisations.lagda.md

@@ -51,9 +51,9 @@ The unit factorisation sends each $X \xto{f} Y$ to $X \xto{\id} X \xto{f} Y$.
 ```agda
 Ff-unit : Factorisation C
 Ff-unit .S₀ (_ , _ , f) = record
-  { map = id
-  ; out = f
-  ; com = intror refl
+  { left    = id
+  ; right   = f
+  ; factors = intror refl
   }
 Ff-unit .S₁ f = record
   { sq₀ = id-comm-sym
@@ -107,10 +107,10 @@ module _ (F G : Factorisation C) where
 
   _⊗ᶠᶠ_ : Factorisation C
   _⊗ᶠᶠ_ .S₀ (_ , _ , f) = record where
-    mid = G.Mid (F.ρ→ f)
-    map = G.λ→ (F.ρ→ f) ∘ F.λ→ f
-    out = G.ρ→ (F.ρ→ f)
-    com = sym (pulll (sym (G.factors _)) ∙ sym (F.factors _))
+    mid     = G.Mid (F.ρ→ f)
+    left    = G.λ→ (F.ρ→ f) ∘ F.λ→ f
+    right   = G.ρ→ (F.ρ→ f)
+    factors = sym (pulll (sym (G.factors _)) ∙ sym (F.factors _))
 
   _⊗ᶠᶠ_ .S₁ sq = record where
     open Interpolant (G .S₁ record { com = S₁ F sq .sq₁ })
@@ -152,10 +152,11 @@ Ff-tensor-functor .F₁ {X , Y} {X' , Y'} (f , g) .com α β h = Interpolant-pat
 Ff-tensor-functor .F-id {_ , Y} = ext λ x y h → elimr refl ∙ annihilate Y (ext refl)
 
 Ff-tensor-functor .F-∘ {X , X'} {Y , Y'} {Z , Z'} f g = ext λ x y h →
-    pulll (sym (f .snd .comᶠᶠ _)) ∙∙ pullr (sym (g .snd .comᶠᶠ _)) ∙∙ sym
-    (ap₂ _∘_ (sym (f .snd .comᶠᶠ _)) (sym (g .snd .comᶠᶠ _))
-  ∙∙ pullr (extendl (sym (g .snd .comᶠᶠ _)))
-  ∙∙ ap₂ _∘_ refl (ap₂ _∘_ refl (collapse X' (ext (refl ,ₚ idl id)))))
+     pulll (sym (f .snd .comᶠᶠ _))
+  ∙∙ pullr (sym (g .snd .comᶠᶠ _))
+  ∙∙ sym (ap₂ _∘_ (sym (f .snd .comᶠᶠ _)) (sym (g .snd .comᶠᶠ _))
+    ∙∙ pullr (extendl (sym (g .snd .comᶠᶠ _)))
+    ∙∙ ap₂ _∘_ refl (ap₂ _∘_ refl (collapse X' (ext (refl ,ₚ idl id)))))
 ```
 
 </details>
@@ -305,8 +306,7 @@ $\eta$ is an easy corollary of initiality for the unit factorisation.
     monoid→unit .is-natural x y f = ext (m.η .comᶠᶠ _ ,ₚ id-comm-sym)
 
     monoid-unit-agrees = ext λ (x , y , f) →
-        intror refl
-      ∙ sym (m.η .sq₀ᶠᶠ f) ,ₚ refl
+      intror refl ∙ sym (m.η .sq₀ᶠᶠ f) ,ₚ refl
 ```
 
 </details>
@@ -343,7 +343,6 @@ multiplication are fixed, this does not matter.
   monoid-on→rwfs-on .R-μ     = monoid→mult
   monoid-on→rwfs-on .R-monad = done where abstract
     done : is-monad F.R-η monoid→mult
-    done = subst
-      (λ e → is-monad e monoid→mult) monoid-unit-agrees
+    done = subst (λ e → is-monad e monoid→mult) monoid-unit-agrees
       monoid-mult-is-monad
 ```