chore: styling

Author: plt-amy

src/Cat/Morphism/Factorisation.lagda.md

@@ -72,8 +72,8 @@ monic.
     → (f-fac : Factorisation C L R f)
     → C.is-monic f
     → C.is-monic (f-fac .left)
-  factor-monic→left-monic {f = f} f-fac f-monic =
-    C.monic-cancell $ C.subst-is-monic (f-fac .factors) f-monic
+  factor-monic→left-monic {f = f} f-fac f-monic = C.monic-cancell $
+    C.subst-is-monic (f-fac .factors) f-monic
 ```
 
 If $f$ is [[epic]] and factors as $f = r \circ l$, then $r$ must also be
@@ -85,6 +85,6 @@ epic.
     → (f-fac : Factorisation C L R f)
     → C.is-epic f
     → C.is-epic (f-fac .right)
-  factor-epic→right-epic {f = f} f-fac f-epic =
-    C.epic-cancelr $ C.subst-is-epic (f-fac .factors) f-epic
+  factor-epic→right-epic {f = f} f-fac f-epic = C.epic-cancelr $
+    C.subst-is-epic (f-fac .factors) f-epic
 ```

src/Cat/Morphism/Factorisation/Orthogonal.lagda.md

@@ -187,14 +187,14 @@ morphism are a proposition.
     q = Univalent.Hom-pathp-refll-iso c-cat {p = isop1p2 .fst} (isop1p2 .snd .snd)
 
     go : x ≡ y
-    go i .mid = c-cat .to-path (isop1p2 .fst) i
-    go i .left = p i
+    go i .mid   = c-cat .to-path (isop1p2 .fst) i
+    go i .left  = p i
     go i .right = q i
 ```
 
 <!--
 ```agda
-    go i .left∈L = is-prop→pathp (λ i → is-tr (L · (p i))) (x .left∈L) (y .left∈L) i
+    go i .left∈L  = is-prop→pathp (λ i → is-tr (L · (p i))) (x .left∈L) (y .left∈L) i
     go i .right∈R = is-prop→pathp (λ i → is-tr (R · (q i))) (x .right∈R) (y .right∈R) i
     go i .factors =
       is-prop→pathp (λ i → C.Hom-set _ _ f (q i C.∘ p i)) (x .factors) (y .factors) i
@@ -227,15 +227,13 @@ technical one.
   L-is-⊥R
     : ∀ {a b} (f : C.Hom a b)
     → (f ∈ L) ≃ (∀ {c d} (m : C.Hom c d) → m ∈ R → Orthogonal C f m)
-  L-is-⊥R f =
-    prop-ext! (λ m f∈L m∈R → to f∈L m m∈R) from
-    where
-      to : ∀ {c d} (m : C.Hom c d) → f ∈ L → m ∈ R → Orthogonal C f m
-      to m f∈L m∈R u v square = L⊥R f f∈L m m∈R u v square
+  L-is-⊥R f = prop-ext! (λ m f∈L m∈R → to f∈L m m∈R) from where
+    to : ∀ {c d} (m : C.Hom c d) → f ∈ L → m ∈ R → Orthogonal C f m
+    to m f∈L m∈R u v square = L⊥R f f∈L m m∈R u v square
 
-      from : (∀ {c d} (m : C.Hom c d) → m ∈ R → Orthogonal C f m) → f ∈ L
-      from ortho = subst (_∈ L) (sym (fa .factors)) $ L-is-stable _ _ m∈L (fa .left∈L)
-        where
+    from : (∀ {c d} (m : C.Hom c d) → m ∈ R → Orthogonal C f m) → f ∈ L
+    from ortho = subst (_∈ L) (sym (fa .factors)) $ L-is-stable _ _ m∈L (fa .left∈L)
+      where
 ```
 
 Suppose that $f$ is left-orthogonal to every $r \in R$, and write out
@@ -261,8 +259,8 @@ and make note of the diagonal filler $g : B \to r(f)$, and that it
 satisfies $gf=e$ and $mg = \id$.
 
 ```agda
-        fa = factor f
-        gpq = ortho (fa .right) (fa .right∈R) (fa .left) C.id (C.idl _ ∙ (fa .factors))
+      fa = factor f
+      gpq = ortho (fa .right) (fa .right∈R) (fa .left) C.id (C.idl _ ∙ (fa .factors))
 ```
 
 We'll show $gr = \id$ by fitting it into a lifting diagram. But
@@ -284,18 +282,18 @@ needed.
 ~~~
 
 ```agda
-        gm=id : gpq .centre .fst C.∘ (fa .right) ≡ C.id
-        gm=id = ap fst $ is-contr→is-prop
-          (L⊥R _ (fa .left∈L) _ (fa .right∈R) _ _ refl)
-          ( _ , C.pullr (sym (fa .factors)) ∙ gpq .centre .snd .fst
-          , C.cancell (gpq .centre .snd .snd)) (C.id , C.idl _ , C.idr _)
+      gm=id : gpq .centre .fst C.∘ (fa .right) ≡ C.id
+      gm=id = ap fst $ is-contr→is-prop
+        (L⊥R _ (fa .left∈L) _ (fa .right∈R) _ _ refl)
+        ( _ , C.pullr (sym (fa .factors)) ∙ gpq .centre .snd .fst
+        , C.cancell (gpq .centre .snd .snd)) (C.id , C.idl _ , C.idr _)
 ```
 
 Think back to the conclusion we wanted to reach: $r$ is in $L$, so since
 $f = r \circ l$ and $R$ is stable, so is $f$!
 
 ```agda
-        m∈L : fa .right ∈ L
-        m∈L = is-iso→in-L (fa .right) $
-          C.make-invertible (gpq .centre .fst) (gpq .centre .snd .snd) gm=id
+      m∈L : fa .right ∈ L
+      m∈L = is-iso→in-L (fa .right) $
+        C.make-invertible (gpq .centre .fst) (gpq .centre .snd .snd) gm=id
 ```

src/Cat/Morphism/Lifts.lagda.md

@@ -171,10 +171,7 @@ aforementioned lifting properties.
     {-# INCOHERENT Lifts-against-arrows-right #-}
 
 open Impl hiding (Lifts; Orthogonal; Lifting) public
-private open module Reimpl {o ℓ} (C : Precategory o ℓ) = Impl {C = C} using (Lifts; Orthogonal; Lifting) public
-{-# DISPLAY Impl.Lifts {C = C} L R = Lifts C L R #-}
-{-# DISPLAY Impl.Orthogonal {C = C} L R = Orthogonal C L R #-}
-{-# DISPLAY Impl.Lifting {C = C} f g h k = Lifting C f g h k #-}
+module _ {o ℓ} (C : Precategory o ℓ) where open Impl {C = C} using (Lifts ; Orthogonal ; Lifting) public
 
 module _ {o ℓ} (C : Precategory o ℓ) where
   open Cat.Reasoning C
@@ -229,8 +226,7 @@ some short calculations show that both triangles commute.
 ```agda
   invertible-left-lifts f f-inv u v vf=gu =
     pure (u ∘ f.inv , cancelr f.invr , pulll (sym vf=gu) ∙ cancelr f.invl)
-    where
-      module f = is-invertible f-inv
+    where module f = is-invertible f-inv
 ```
 
 <details>
@@ -240,8 +236,7 @@ some short calculations show that both triangles commute.
 ```agda
   invertible-right-lifts g g-inv u v vf=gu =
     pure (g.inv ∘ v , pullr vf=gu ∙ cancell g.invr , cancell g.invl)
-    where
-      module g = is-invertible g-inv
+    where module g = is-invertible g-inv
 ```
 </details>
 
@@ -371,8 +366,8 @@ type of lifts of such a square is a proposition.
 ```agda
   left-epic→lift-is-prop
     : is-epic f → v ∘ f ≡ g ∘ u → is-prop (Lifting C f g u v)
-  left-epic→lift-is-prop f-epi vf=gu (l , lf=u , _) (k , kf=u , _) =
-    Σ-prop-path! (f-epi l k (lf=u ∙ sym kf=u))
+  left-epic→lift-is-prop f-epi vf=gu (l , lf=u , _) (k , kf=u , _) = Σ-prop-path! $
+    f-epi l k (lf=u ∙ sym kf=u)
 ```
 
 Dually, if $g$ is a [[monomorphism]], then we the type of lifts is also

src/Cat/Morphism/Orthogonal.lagda.md

@@ -72,26 +72,33 @@ $!_X : X \to 1$ is the unique map from $X$ into the [[terminal object]].
 The proof is mostly a calculation, so we present it without a lot of comment.
 
 ```agda
-  object-orthogonal-!-orthogonal {X = X} T f =
-    prop-ext! fwd bwd
-    where
-      module T = Terminal T
-
-      fwd : Orthogonal C f X → Orthogonal C f (! T)
-      fwd f⊥X u v sq .centre = f⊥X u .centre .fst , f⊥X u .centre .snd , T.!-unique₂ _ _
-      fwd f⊥X u v sq .paths m = Σ-prop-path! (ap fst (f⊥X u .paths (m .fst , m .snd .fst)))
-
-      bwd : Orthogonal C f (! T) → Orthogonal C f X
-      bwd f⊥! u .centre =  f⊥! u T.! (T.!-unique₂ _ _) .centre .fst , f⊥! u T.! (T.!-unique₂ _ _) .centre .snd .fst
-      bwd f⊥! u .paths (w , eq) = Σ-prop-path! (ap fst (f⊥! _ _ _ .paths (w , eq , (T.!-unique₂ _ _))))
+  object-orthogonal-!-orthogonal {X = X} T f = prop-ext! fwd bwd where
+    module T = Terminal T
+
+    fwd : Orthogonal C f X → Orthogonal C f T.!
+    fwd f⊥X u v sq .centre =
+        f⊥X u .centre .fst
+      , f⊥X u .centre .snd
+      , T.!-unique₂ _ _
+    fwd f⊥X u v sq .paths m = Σ-prop-path! $
+      ap fst (f⊥X u .paths (m .fst , m .snd .fst))
+
+    bwd : Orthogonal C f (! T) → Orthogonal C f X
+    bwd f⊥! u .centre =
+        f⊥! u T.! (T.!-unique₂ _ _) .centre .fst
+      , f⊥! u T.! (T.!-unique₂ _ _) .centre .snd .fst
+    bwd f⊥! u .paths (w , eq) = Σ-prop-path! $
+      ap fst (f⊥! _ _ _ .paths (w , eq , (T.!-unique₂ _ _)))
 ```
 
 As a passing observation we note that if $f \ortho X$ and $X \cong Y$,
 then $f \ortho Y$. Of course, this is immediate in categories, but it
 holds in the generality of precategories.
 
 ```agda
-  obj-orthogonal-iso : ∀ {a b} {X Y} (f : Hom a b) → X ≅ Y → Orthogonal C f X → Orthogonal C f Y
+  obj-orthogonal-iso
+    : ∀ {a b} {X Y} (f : Hom a b)
+    → X ≅ Y → Orthogonal C f X → Orthogonal C f Y
 ```
 
 <!--
@@ -113,11 +120,11 @@ A slightly more interesting lemma is that, if $f$ is orthogonal to
 itself, then it is an isomorphism:
 
 ```agda
-  self-orthogonal→invertible : ∀ {a b} (f : Hom a b) → Orthogonal C f f → is-invertible f
+  self-orthogonal→invertible
+    : ∀ {a b} (f : Hom a b) → Orthogonal C f f → is-invertible f
   self-orthogonal→invertible f f⊥f =
-    make-invertible (gpq .fst) (gpq .snd .snd) (gpq .snd .fst)
-    where
-      gpq = f⊥f id id (idl _ ∙ intror refl) .centre
+    let (f , p , q) = f⊥f id id (idl _ ∙ intror refl) .centre in
+    make-invertible f q p
 ```
 
 If $f$ is an epi or $g$ is a mono, then the mere existence of
@@ -127,23 +134,25 @@ _any_ lift is enough to establish that $f \ortho g$.
   left-epic-lift→orthogonal
     : (g : Hom c d)
     → is-epic f → Lifts C f g → Orthogonal C f g
-  left-epic-lift→orthogonal g f-epi lifts u v vf=gu =
-    is-prop∥∥→is-contr (left-epic→lift-is-prop C f-epi vf=gu) (lifts u v vf=gu)
+  left-epic-lift→orthogonal g f-epi lifts u v vf=gu = is-prop∥∥→is-contr
+    (left-epic→lift-is-prop C f-epi vf=gu)
+    (lifts u v vf=gu)
 
   right-monic-lift→orthogonal
     : (f : Hom a b)
     → is-monic g → Lifts C f g → Orthogonal C f g
-  right-monic-lift→orthogonal f g-mono lifts u v vf=gu =
-    is-prop∥∥→is-contr (right-monic→lift-is-prop C g-mono vf=gu) (lifts u v vf=gu)
+  right-monic-lift→orthogonal f g-mono lifts u v vf=gu = is-prop∥∥→is-contr
+    (right-monic→lift-is-prop C g-mono vf=gu)
+    (lifts u v vf=gu)
 ```
 
 <!--
 ```agda
   left-epic-lift→orthogonal-class
     : ∀ {κ} (R : Arrows C κ)
     → is-epic f → Lifts C f R → Orthogonal C f R
-  left-epic-lift→orthogonal-class R f-epic lifts r r∈R =
-    left-epic-lift→orthogonal r f-epic (lifts r r∈R)
+  left-epic-lift→orthogonal-class R f-epic lifts r r∈R = left-epic-lift→orthogonal
+    r f-epic (lifts r r∈R)
 
   right-monic-lift→orthogonal-class
     : ∀ {κ} (L : Arrows C κ)
@@ -159,13 +168,13 @@ other morphism.
 ```agda
   invertible→left-orthogonal : (g : Hom c d) → Orthogonal C Isos g
   invertible→left-orthogonal g f f-inv =
-    left-epic-lift→orthogonal g (invertible→epic f-inv) $
-    invertible-left-lifts C f f-inv
+      left-epic-lift→orthogonal g (invertible→epic f-inv)
+    $ invertible-left-lifts C f f-inv
 
   invertible→right-orthogonal : (f : Hom a b) → Orthogonal C f Isos
   invertible→right-orthogonal f g g-inv =
-    right-monic-lift→orthogonal f (invertible→monic g-inv) $
-    invertible-right-lifts C g g-inv
+      right-monic-lift→orthogonal f (invertible→monic g-inv)
+    $ invertible-right-lifts C g g-inv
 ```
 
 Phrased another way, the class of isomorphisms is left and right orthogonal
@@ -244,8 +253,7 @@ the object. Given a map $a : a \to \iota X$,
   in-subcategory→orthogonal-to-inverted
     : ∀ {X} {a b} {f : C.Hom a b} → D.is-invertible (r.₁ f) → Orthogonal C f (ι.₀ X)
   in-subcategory→orthogonal-to-inverted {X} {A} {B} {f} rf-inv a→x =
-    contr (fact , factors) λ { (g , factors') →
-      Σ-prop-path! (h≡k factors factors') }
+    contr (fact , factors) λ { (g , factors') → Σ-prop-path! (h≡k factors factors') }
     where
       module rf = D.is-invertible rf-inv
       module η⁻¹ {a} = C.is-invertible (is-reflective→unit-right-is-iso r⊣ι ι-ff {a})
@@ -325,13 +333,13 @@ the subcategory:
   orthogonal-to-ηs→in-subcategory
     : ∀ {X} → (∀ B → Orthogonal C (unit.η B) X) → C.is-invertible (unit.η X)
   orthogonal-to-ηs→in-subcategory {X} ortho =
-    C.make-invertible x lemma (ortho X C.id .centre .snd)
-    where
+    C.make-invertible x lemma (ortho X C.id .centre .snd) where
       x = ortho X C.id .centre .fst
-      lemma = unit.η _ C.∘ x             ≡⟨ unit.is-natural _ _ _ ⟩
-              ιr.₁ x C.∘ unit.η (ιr.₀ X) ≡⟨ C.refl⟩∘⟨ η-comonad-commute r⊣ι ι-ff ⟩
-              ιr.₁ x C.∘ ιr.₁ (unit.η X) ≡⟨ ιr.annihilate (ortho X C.id .centre .snd) ⟩
-              C.id                       ∎
+      lemma =
+        unit.η _ C.∘ x             ≡⟨ unit.is-natural _ _ _ ⟩
+        ιr.₁ x C.∘ unit.η (ιr.₀ X) ≡⟨ C.refl⟩∘⟨ η-comonad-commute r⊣ι ι-ff ⟩
+        ιr.₁ x C.∘ ιr.₁ (unit.η X) ≡⟨ ιr.annihilate (ortho X C.id .centre .snd) ⟩
+        C.id                       ∎
 ```
 
 And the converse to *that* is a specialisation of the first thing we
@@ -344,6 +352,8 @@ which $\eta$ is an isomorphism.
   in-subcategory→orthogonal-to-ηs
     : ∀ {X B} → C.is-invertible (unit.η X) → Orthogonal C (unit.η B) X
   in-subcategory→orthogonal-to-ηs inv =
-    obj-orthogonal-iso C (unit.η _) (C.invertible→iso _ (C.is-invertible-inverse inv)) $
-    in-subcategory→orthogonal-to-inverted (is-reflective→left-unit-is-iso r⊣ι ι-ff)
+      obj-orthogonal-iso C (unit.η _)
+        (C.invertible→iso _ (C.is-invertible-inverse inv))
+    $ in-subcategory→orthogonal-to-inverted
+        (is-reflective→left-unit-is-iso r⊣ι ι-ff)
 ```