chore: refactor liftings & orthogonality (the1lab#555)

This PR refactors the APIs for lifting and orthogonality properties, and
also redefines projective/injective objects in
terms of lifts. I've also made some minor code improvements along the
way, like pulling out `Factorisation` into its own module. Closes the1lab#552.

---------

Co-authored-by: Amélia <[email protected]>
Co-authored-by: Naïm Camille Favier <[email protected]>

Author: 3 people

src/1Lab/Truncation.lagda.md

@@ -222,6 +222,13 @@ from the HoTT book. For example, a type $X$ is said _merely equivalent_
 to $Y$ if the type $\| X \equiv Y \|$ is inhabited.
 :::
 
+<!--
+```agda
+is-prop∥∥→is-contr : ∀ {ℓ} {P : Type ℓ} → is-prop P → ∥ P ∥ → is-contr P
+is-prop∥∥→is-contr pprop mp = is-prop∙→is-contr pprop (∥-∥-out pprop mp)
+```
+-->
+
 ## Maps into sets
 
 The elimination principle for $\| A \|$ says that we can only use the

src/Borceux.lagda.md

@@ -10,6 +10,7 @@ open import Algebra.Group.Cat.Base
 open import Algebra.Group.Free hiding (_◆_)
 open import Algebra.Group.Ab
 
+open import Cat.Morphism.Factorisation.Orthogonal
 open import Cat.Diagram.Coequaliser.RegularEpi
 open import Cat.Functor.Adjoint.Epireflective
 open import Cat.Functor.Adjoint.Representable
@@ -89,6 +90,7 @@ open import Cat.Instances.Slice
 open import Cat.Functor.Closed
 open import Cat.Instances.Free
 open import Cat.Instances.Sets
+open import Cat.Morphism.Lifts
 open import Cat.Diagram.Monad
 open import Cat.Functor.Final
 open import Cat.Functor.Joint
@@ -786,7 +788,7 @@ _ = Karoubi-is-completion
 ```agda
 _ = is-regular-epi
 _ = is-strong-epi
-_ = strong-epi-∘
+_ = ∘-is-strong-epic
 _ = strong-epi-cancelr
 _ = strong-epi+mono→invertible
 _ = is-regular-epi→is-strong-epi
@@ -799,7 +801,7 @@ _ = is-extremal-epi→is-strong-epi
 * Definition 4.3.1: `is-regular-epi`{.Agda}
 * Definition 4.3.5: `is-strong-epi`{.Agda}
 * Proposition 4.3.6:
-  * 1. `strong-epi-∘`{.Agda}
+  * 1. `∘-is-strong-epic`{.Agda}
   * 2. `strong-epi-cancelr`{.Agda}
   * 3. `strong-epi-mono→invertible`{.Agda}
   * 4. `is-regular-epi→is-strong-epi`{.Agda}
@@ -954,9 +956,7 @@ _ = Localisation
 
 <!--
 ```agda
-_ = m⊥m
-_ = m⊥o
-_ = o⊥m
+_ = Orthogonal
 _ = object-orthogonal-!-orthogonal
 _ = in-subcategory→orthogonal-to-inverted
 _ = orthogonal-to-ηs→in-subcategory
@@ -966,8 +966,8 @@ _ = in-subcategory→orthogonal-to-ηs
 
 * Definition 5.4.1: `m⊥m`{.Agda}
 * Definition 5.4.2:
-  1. `m⊥o`{.Agda}
-  2. `o⊥m`{.Agda}
+  1. `Orthogonal`{.Agda}
+  2. `Orthogonal`{.Agda}
 * Proposition 5.4.3: `object-orthogonal-!-orthogonal`{.Agda}
 * Proposition 5.4.4:
   * 1.
@@ -978,9 +978,9 @@ _ = in-subcategory→orthogonal-to-ηs
 
 <!--
 ```agda
-_ = is-factorisation-system
+_ = is-ofs
 _ = factorisation-essentially-unique
-_ = E-is-⊥M
+_ = L-is-⊥R
 _ = in-intersection≃is-iso
 ```
 -->
@@ -1116,5 +1116,3 @@ _ = const-nato
 * Exercise 8.4.6:
   * (⇒) `dependent-product→lcc`{.Agda}
   * (⇐) `lcc→dependent-product`{.Agda}
-
-[[marked graph homomorphism]]

src/Cat/Bi/Instances/Relations.lagda.md

@@ -201,10 +201,10 @@ into a subobject.]
   open Relation t renaming (src to t₁ ; tgt to t₂) hiding (rel)
 
   i : ∀ {x y} {f : Hom x y} → Hom im[ f ] y
-  i = factor _ .forget
+  i = factor _ .right
 
   q : ∀ {x y} {f : Hom x y} → Hom x im[ f ]
-  q = factor _ .mediate
+  q = factor _ .left
 
   ξ₁ = [rs]t.inter .p₁
   ξ₂ = [rs]t.inter .p₂
@@ -374,7 +374,7 @@ Since $q$ is a strong epi, $\alpha$ is, too.
     α-is-pb = pasting-outer→left-is-pullback ([rs]t.inter .has-is-pb) rem₁ ([rs]t.inter .p₂∘universal)
 
   α-cover : is-strong-epi C α
-  α-cover = stable _ _ (□-out! (factor rs.it .mediate∈E)) α-is-pb
+  α-cover = stable _ _ (factor rs.it .left∈L) α-is-pb
 ```
 
 The purpose of all this calculation is the following: Postcomposing with
@@ -433,7 +433,7 @@ want to look at the formalisation.
       (r[st].inter .p₁∘universal)
 
   β-cover : is-strong-epi C β
-  β-cover = stable _ _ (□-out! (factor st.it .mediate∈E)) β-is-pb
+  β-cover = stable _ _ (factor st.it .left∈L) β-is-pb
 
   r[st]≅i : Im r[st].it Sub.≅ Im j
   r[st]≅i = subst (λ e → Im r[st].it Sub.≅ Im e)
@@ -474,7 +474,7 @@ but keep in mind that they are not commented.
 ```agda
 ∘-rel-monotone {r = r} {r'} {s} {s'} α β =
   Im-universal (∘-rel.it r s) _
-    {e = factor _ .mediate ∘ ∘-rel.inter r' s' .universal
+    {e = factor _ .left ∘ ∘-rel.inter r' s' .universal
       {p₁' = β .map ∘ ∘-rel.inter _ _ .p₁}
       {p₂' = α .map ∘ ∘-rel.inter _ _ .p₂}
       ( pullr (pulll (sym (β .com) ∙ idl _))
@@ -497,7 +497,7 @@ but keep in mind that they are not commented.
     (assoc _ _ _)
 
   f≤fid : f ≤ₘ ∘-rel f id-rel
-  f≤fid .map = factor _ .mediate ∘
+  f≤fid .map = factor _ .left ∘
     ∘-rel.inter f id-rel .universal {p₁' = Relation.src f} {p₂' = id}
       (eliml π₂∘⟨⟩ ∙ intror refl)
   f≤fid .com = idl _ ∙ sym (pulll (sym (factor _ .factors)) ∙ ⟨⟩∘ _ ∙ sym (⟨⟩-unique
@@ -511,7 +511,7 @@ but keep in mind that they are not commented.
     (assoc _ _ _ ∙ ∘-rel.inter id-rel f .square ∙ eliml π₁∘⟨⟩ ∙ introl π₂∘⟨⟩)
 
   f≤idf : f ≤ₘ ∘-rel id-rel f
-  f≤idf .map = factor _ .mediate ∘
+  f≤idf .map = factor _ .left ∘
     ∘-rel.inter id-rel f .universal {p₁' = id} {p₂' = Relation.tgt f}
       (idr _ ∙ sym (eliml π₁∘⟨⟩))
   f≤idf .com = idl _ ∙ sym (pulll (sym (factor _ .factors)) ∙ ⟨⟩∘ _ ∙ sym (⟨⟩-unique

src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md

@@ -143,7 +143,7 @@ module _ {o ℓ oj ℓj}
   {C : Precategory o ℓ} {J : Precategory oj ℓj}
   {F : Functor J C}
   (∐Ob : has-coproducts-indexed-by C ⌞ J ⌟)
-  (∐Hom : has-coproducts-indexed-by C (Arrows J))
+  (∐Hom : has-coproducts-indexed-by C (Arrow J))
   (∐F : Colimit F)
   where
 ```

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

@@ -578,10 +578,10 @@ module _ {o ℓ} {C : Precategory o ℓ} where
   colimit-as-coequaliser-of-coproduct
     : ∀ {oj ℓj} {J : Precategory oj ℓj}
     → has-coproducts-indexed-by C ⌞ J ⌟
-    → has-coproducts-indexed-by C (Arrows J)
+    → has-coproducts-indexed-by C (Arrow J)
     → has-coequalisers C
     → (F : Functor J C) → Colimit F
-  colimit-as-coequaliser-of-coproduct {oj} {ℓj} {J} has-Ob-cop has-Arrows-cop has-coeq F =
+  colimit-as-coequaliser-of-coproduct {oj} {ℓj} {J} has-Ob-cop has-Arrow-cop has-coeq F =
     to-colimit (to-is-colimit colim) where
 ```
 
@@ -616,15 +616,15 @@ and the second morphism to be the injection into the codomain component precompo
 
 ~~~{.quiver}
 \[\begin{tikzcd}
-	{\displaystyle \coprod_{(f : a \to b) : \text{Arrows}(\mathcal J)} F(a)} & {\displaystyle \coprod_{o : \text{Ob}(\mathcal J)} F(o)}
+	{\displaystyle \coprod_{(f : a \to b) : \text{Arrow}(\mathcal J)} F(a)} & {\displaystyle \coprod_{o : \text{Ob}(\mathcal J)} F(o)}
 	\arrow["{\iota_a}", shift left, from=1-1, to=1-2]
 	\arrow["{\iota_b \circ F(f)}"', shift right, from=1-1, to=1-2]
 \end{tikzcd}\]
 ~~~
 
 ```agda
-    Dom : Indexed-coproduct C {Idx = Arrows J} λ (a , b , f) → F₀ a
-    Dom = has-Arrows-cop _
+    Dom : Indexed-coproduct C {Idx = Arrow J} λ (a , b , f) → F₀ a
+    Dom = has-Arrow-cop _
 
     s t : C.Hom (Dom .ΣF) (Obs .ΣF)
     s = Dom .match λ (a , b , f) → Obs .ι b C.∘ F₁ f

src/Cat/Diagram/Injective.lagda.md

@@ -10,6 +10,7 @@ open import Cat.Diagram.Pullback.Along
 open import Cat.Diagram.Pullback
 open import Cat.Functor.Morphism
 open import Cat.Diagram.Product
+open import Cat.Morphism.Lifts
 open import Cat.Diagram.Omega
 open import Cat.Functor.Hom
 open import Cat.Prelude hiding (Ω; true)
@@ -65,9 +66,7 @@ relative to monomorphisms in $\cC$.
 
 ```agda
 is-injective : (A : Ob) → Type _
-is-injective A =
-  ∀ {X Y} (i : Hom X A) (m : X ↪ Y)
-  → ∃[ r ∈ Hom Y A ] (r ∘ m .mor ≡ i)
+is-injective A = Lifts C Monos A
 ```
 
 Classically, injective objects are usually very easy to find. For example.
@@ -98,10 +97,10 @@ epis. This directly gives us the factorization we need!
 preserves-epis→injective
   : preserves-epis (Hom-into C A)
   → is-injective A
-preserves-epis→injective {A = A} hom-epi {X = X} {Y = Y} i m =
+preserves-epis→injective {A = A} hom-epi {X} {Y} m m-monic i =
   epi→surjective (el! (Hom Y A)) (el! (Hom X A))
-    (_∘ m .mor)
-    (λ {c} → hom-epi (m .monic) {c = c})
+    (_∘ m)
+    (λ {c} → hom-epi m-monic {c = c})
     i
 ```
 
@@ -122,7 +121,7 @@ injective→preserves-epis inj {f = m} m-mono g h p =
       g (r ∘ m)  ≡⟨ p $ₚ r ⟩
       h (r ∘ m)  ≡⟨ ap h r-retract ⟩
       h k  ∎)
-      (inj k (make-mono m m-mono))
+      (inj m m-mono k)
 ```
 
 ## Closure of injectives
@@ -180,9 +179,9 @@ $\pi_2 \circ \langle r_1 , r_2 \rangle \circ m = r_2 \circ m = i$, so $\langle r
 is a valid extension.
 
 ```agda
-product-injective {π₁ = π₁} {π₂ = π₂} A-inj B-inj prod i m = do
-  (r₁ , r₁-factor) ← A-inj (π₁ ∘ i) m
-  (r₂ , r₂-factor) ← B-inj (π₂ ∘ i) m
+product-injective {π₁ = π₁} {π₂ = π₂} A-inj B-inj prod m m-monic i = do
+  (r₁ , r₁-factor) ← A-inj m m-monic (π₁ ∘ i)
+  (r₂ , r₂-factor) ← B-inj m m-monic (π₂ ∘ i)
   pure (⟨ r₁ , r₂ ⟩ , unique₂ (pulll π₁∘⟨⟩) (pulll π₂∘⟨⟩) (sym r₁-factor) (sym r₂-factor))
   where open is-product prod
 ```
@@ -223,11 +222,11 @@ each extension $r_i$ for each $i : I$, whereas we need the mere existence of
 but we can avoid this by requiring that $I$ be set-projective.
 
 ```agda
-indexed-coproduct-projective {Aᵢ = Aᵢ} {π = π} Idx-pro Aᵢ-inj prod {X = X} {Y = Y} ι m = do
+indexed-coproduct-projective {Aᵢ = Aᵢ} {π = π} Idx-pro Aᵢ-inj prod {X} {Y} m m-monic ι = do
   r ← Idx-pro
-    (λ i → Σ[ rᵢ ∈ Hom Y (Aᵢ i) ] rᵢ ∘ m .mor ≡ π i ∘ ι)
+    (λ i → Σ[ rᵢ ∈ Hom Y (Aᵢ i) ] rᵢ ∘ m ≡ π i ∘ ι)
     (λ _ → hlevel 2)
-    (λ i → Aᵢ-inj i (π i ∘ ι) m)
+    (λ i → Aᵢ-inj i m m-monic (π i ∘ ι))
   pure (tuple (λ i → r i .fst) , unique₂ (λ i → pulll commute ∙ r i .snd))
   where open is-indexed-product prod
 ```
@@ -241,8 +240,8 @@ section→injective
   → (r : Hom A S)
   → has-section r
   → is-injective S
-section→injective A-inj r s i m = do
-  (t , t-factor) ← A-inj (s .section ∘ i) m
+section→injective A-inj r s m m-monic i = do
+  (t , t-factor) ← A-inj m m-monic (s .section ∘ i)
   pure (r ∘ t , pullr t-factor ∙ cancell (s .is-section))
 ```
 
@@ -272,7 +271,7 @@ consider the following extension problem.
 ~~~
 
 ```agda
-Ω-injective {Ω = Ω} {true = true} pullbacks Ω-subobj {X} {Y} i m =
+Ω-injective {Ω = Ω} {true = true} pullbacks Ω-subobj {X} {Y} m m-monic i =
   pure extension
   where
     open is-generic-subobject Ω-subobj
@@ -312,7 +311,7 @@ $X$, which we can then compose with $m$ to get a subobject of $Y$.
     [i] = named i
 
     m∩[i] : Subobject Y
-    m∩[i] = cutₛ (∘-is-monic (m .monic) ([i] .monic))
+    m∩[i] = cutₛ (∘-is-monic m-monic ([i] .monic))
 ```
 
 We can then classify our subobject $m \circ [i]$ to get a map
@@ -364,13 +363,13 @@ This means that $\mathrm{name}(m \circ [i]) \circ m = i$, which completes
 the proof.
 
 ```agda
-    extension : Σ[ i* ∈ Hom Y Ω ] i* ∘ m .mor ≡ i
+    extension : Σ[ i* ∈ Hom Y Ω ] i* ∘ m ≡ i
     extension .fst = name m∩[i]
     extension .snd =
       Ω-unique₂ $
       paste-is-pullback-along
         (classifies m∩[i])
-        (is-pullback-along-monic (m .monic))
+        (is-pullback-along-monic m-monic)
         refl
 ```
 

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

@@ -716,10 +716,10 @@ module _ {o ℓ} {C : Precategory o ℓ} where
   limit-as-equaliser-of-product
     : ∀ {oj ℓj} {J : Precategory oj ℓj}
     → has-products-indexed-by C ⌞ J ⌟
-    → has-products-indexed-by C (Arrows J)
+    → has-products-indexed-by C (Arrow J)
     → has-equalisers C
     → (F : Functor J C) → Limit F
-  limit-as-equaliser-of-product {oj} {ℓj} {J} has-Ob-prod has-Arrows-prod has-eq F =
+  limit-as-equaliser-of-product {oj} {ℓj} {J} has-Ob-prod has-Arrow-prod has-eq F =
     to-limit (to-is-limit lim) where
 ```
 
@@ -753,15 +753,15 @@ and the second morphism to be the projection of the domain postcomposed with $f$
 
 ~~~{.quiver}
 \[\begin{tikzcd}
-	{\displaystyle \prod_{o : \text{Ob}(\mathcal J)} F(o)} & {\displaystyle \prod_{(f : a \to b) : \text{Arrows}(\mathcal J)} F(b)}
+	{\displaystyle \prod_{o : \text{Ob}(\mathcal J)} F(o)} & {\displaystyle \prod_{(f : a \to b) : \text{Arrow}(\mathcal J)} F(b)}
 	\arrow["{\pi_b}", shift left, from=1-1, to=1-2]
 	\arrow["{F(f) \circ \pi_a}"', shift right, from=1-1, to=1-2]
 \end{tikzcd}\]
 ~~~
 
 ```agda
-    Cod : Indexed-product C {Idx = Arrows J} λ (a , b , f) → F₀ b
-    Cod = has-Arrows-prod _
+    Cod : Indexed-product C {Idx = Arrow J} λ (a , b , f) → F₀ b
+    Cod = has-Arrow-prod _
 
     s t : C.Hom (Obs .ΠF) (Cod .ΠF)
     s = Cod .tuple λ (a , b , f) → F₁ f C.∘ Obs .π a

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

@@ -103,7 +103,7 @@ products).
   Finitely-complete→is-finitely-complete cat Flim finite =
     limit-as-equaliser-of-product
       (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Ob))
-      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Arrows))
+      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Arrow))
       (Flim .equalisers)
 
   is-finitely-complete→Finitely-complete