diff --git a/src/Cat/Bi/Diagram/Monad.lagda.md b/src/Cat/Bi/Diagram/Monad.lagda.md
index bcf495e3b..20988dfa8 100644
--- a/src/Cat/Bi/Diagram/Monad.lagda.md
+++ b/src/Cat/Bi/Diagram/Monad.lagda.md
@@ -105,6 +105,7 @@ compatibility paths have to be adjusted slightly. Check it out below:
```agda
module _ {o ℓ} {C : Precategory o ℓ} where
open Cat.Monad-on
+ open Cat.is-monad
open Monad
private module C = Cr C
@@ -115,13 +116,13 @@ module _ {o ℓ} {C : Precategory o ℓ} where
monad' : Cat.Monad-on M.M
monad' .unit = M.η
monad' .mult = M.μ
- monad' .μ-unitr {x} =
+ monad' .has-is-monad .μ-unitr {x} =
ap (M.μ ._=>_.η x C.∘_) (C.intror refl)
∙ M.μ-unitr ηₚ x
- monad' .μ-unitl {x} =
+ monad' .has-is-monad .μ-unitl {x} =
ap (M.μ ._=>_.η x C.∘_) (C.introl (M.M .Functor.F-id))
∙ M.μ-unitl ηₚ x
- monad' .μ-assoc {x} =
+ monad' .has-is-monad .μ-assoc {x} =
ap (M.μ ._=>_.η x C.∘_) (C.intror refl)
∙∙ M.μ-assoc ηₚ x
∙∙ ap (M.μ ._=>_.η x C.∘_) (C.elimr refl ∙ C.eliml (M.M .Functor.F-id))
diff --git a/src/Cat/Diagram/Comonad.lagda.md b/src/Cat/Diagram/Comonad.lagda.md
index 3db23b985..689795cd1 100644
--- a/src/Cat/Diagram/Comonad.lagda.md
+++ b/src/Cat/Diagram/Comonad.lagda.md
@@ -28,29 +28,27 @@ A **comonad on a category** $\cC$ is dual to a [[monad]] on $\cC$; instead
of a unit $\Id \To M$ and multiplication $(M \circ M) \To M$, we have a
counit $W \To \Id$ and comultiplication $W \To (W \circ W)$. More
generally, we can define what it means to equip a *fixed* functor $W$
-with the structure of a comonad.
+with the structure of a comonad; even more generally, we can specify
+what it means for a triple $(W, \eps, \delta)$ to be a comonad.
+Unsurprisingly, these are dual to the equations of a monad.
```agda
- record Comonad-on (W : Functor C C) : Type (o ⊔ ℓ) where
- field
- counit : W => Id
- comult : W => (W F∘ W)
+ record is-comonad {W : Functor C C} (counit : W => Id) (comult : W => W F∘ W) : Type (o ⊔ ℓ) where
```
-We also have equations governing the counit and comultiplication.
-Unsurprisingly, these are dual to the equations of a monad.
-
```agda
field
δ-unitl : ∀ {x} → W₁ (ε x) ∘ δ x ≡ id
@@ -58,6 +56,22 @@ Unsurprisingly, these are dual to the equations of a monad.
δ-assoc : ∀ {x} → W₁ (δ x) ∘ δ x ≡ δ (W₀ x) ∘ δ x
```
+```agda
+ record Comonad-on (W : Functor C C) : Type (o ⊔ ℓ) where
+ field
+ counit : W => Id
+ comult : W => (W F∘ W)
+ has-is-comonad : is-comonad counit comult
+```
+
+
+
-Furthermore, these natural transformations must satisfy identity and
-associativity laws exactly analogous to those of a monoid.
-
```agda
field
μ-unitr : ∀ {x} → μ x C.∘ M₁ (η x) ≡ C.id
@@ -78,6 +70,18 @@ associativity laws exactly analogous to those of a monoid.
μ-assoc : ∀ {x} → μ x C.∘ M₁ (μ x) ≡ μ x C.∘ μ (M₀ x)
```
+[monoid]: Algebra.Monoid.html
+
+```agda
+ record Monad-on (M : Functor C C) : Type (o ⊔ h) where
+ no-eta-equality
+ field
+ unit : Id => M
+ mult : M F∘ M => M
+ has-is-monad : is-monad unit mult
+ open is-monad has-is-monad public
+```
+
# Algebras over a monad {defines="monad-algebra algebra-over-a-monad algebras-over-a-monad"}
One way of interpreting a monad $M$ is as giving a _signature_ for an
@@ -121,6 +125,8 @@ doesn't matter whether you first join then evaluate, or evaluate twice.
→ PathP (λ i → Algebra-on M (p i)) A B
Algebra-on-pathp over mults = injectiveP (λ _ → eqv) (mults ,ₚ prop!)
+unquoteDecl H-Level-is-monad = declare-record-hlevel 1 H-Level-is-monad (quote is-monad)
+
instance
Extensional-Algebra-on
: ∀ {o ℓ ℓr} {C : Precategory o ℓ} {F : Functor C C} {M : Monad-on F}
diff --git a/src/Cat/Diagram/Monad/Codensity.lagda.md b/src/Cat/Diagram/Monad/Codensity.lagda.md
index d9b63c08c..c470169fc 100644
--- a/src/Cat/Diagram/Monad/Codensity.lagda.md
+++ b/src/Cat/Diagram/Monad/Codensity.lagda.md
@@ -20,6 +20,7 @@ private variable
o ℓ : Level
A B : Precategory o ℓ
open Monad-on
+open is-monad
open _=>_
```
-->
@@ -123,7 +124,7 @@ construct auxiliary natural transformations representing each pair of
maps we want to compute with.
```agda
- Codensity .μ-unitr {x = x} = path ηₚ x where
+ Codensity .has-is-monad .μ-unitr {x = x} = path ηₚ x where
nat₁ : Ext => Ext
nat₁ .η x = σ mult-nt .η x B.∘ Ext.₁ (σ unit-nt .η x)
nat₁ .is-natural x y f = Ext.extendr (σ unit-nt .is-natural x y f)
@@ -137,7 +138,7 @@ maps we want to compute with.
∙ Ext.cancelr (σ-comm ηₚ x)))
(ext λ _ → B.intror refl)
- Codensity .μ-unitl {x = x} = path ηₚ x where
+ Codensity .has-is-monad .μ-unitl {x = x} = path ηₚ x where
nat₁ : Ext => Ext
nat₁ .η x = σ mult-nt .η x B.∘ σ unit-nt .η (Ext.₀ x)
nat₁ .is-natural x y f = B.extendr (σ unit-nt .is-natural _ _ _)
@@ -152,7 +153,7 @@ maps we want to compute with.
∙∙ B.cancell (σ-comm ηₚ x))
(ext λ _ → B.intror refl)
- Codensity .μ-assoc {x = x} = path ηₚ x where
+ Codensity .has-is-monad .μ-assoc {x = x} = path ηₚ x where
mult' : (Ext F∘ Ext F∘ Ext) F∘ F => F
mult' .η x = eps .η x B.∘ Ext.₁ (mult-nt .η x)
mult' .is-natural x y f = Ext.extendr (mult-nt .is-natural _ _ _)
diff --git a/src/Cat/Diagram/Monad/Extension.lagda.md b/src/Cat/Diagram/Monad/Extension.lagda.md
index 03d482b16..015f2c41d 100644
--- a/src/Cat/Diagram/Monad/Extension.lagda.md
+++ b/src/Cat/Diagram/Monad/Extension.lagda.md
@@ -168,6 +168,7 @@ bolting together our results from the previous section.
Extension-system→Monad E = _ , monad where
module E = Extension-system E
open Monad-on
+ open is-monad
monad : Monad-on E.M
monad .unit .η x = E.unit
@@ -179,15 +180,15 @@ bolting together our results from the previous section.
The monad laws follow from another short series of computations.
```agda
- monad .μ-unitr =
+ monad .has-is-monad .μ-unitr =
E.bind id ∘ E.bind (E.unit ∘ E.unit) ≡⟨ E.bind-∘ _ _ ⟩
E.bind (E.bind id ∘ E.unit ∘ E.unit) ≡⟨ ap E.bind (cancell (E.bind-unit-∘ id)) ⟩
E.bind E.unit ≡⟨ E.bind-unit-id ⟩
id ∎
- monad .μ-unitl =
+ monad .has-is-monad .μ-unitl =
E.bind id ∘ E.unit ≡⟨ E.bind-unit-∘ id ⟩
id ∎
- monad .μ-assoc =
+ monad .has-is-monad .μ-assoc =
E.bind id ∘ E.bind (E.unit ∘ E.bind id) ≡⟨ E.bind-∘ _ _ ⟩
E.bind (E.bind id ∘ E.unit ∘ E.bind id) ≡⟨ ap E.bind (cancell (E.bind-unit-∘ id) ∙ sym (idr _)) ⟩
E.bind (E.bind id ∘ id) ≡˘⟨ E.bind-∘ _ _ ⟩
diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md
index 7d8cc2304..fe4a3d207 100644
--- a/src/Cat/Displayed/Comprehension.lagda.md
+++ b/src/Cat/Displayed/Comprehension.lagda.md
@@ -442,6 +442,7 @@ Comprehension→comonad fib P = comp-comonad where
open Cartesian-fibration E fib
open Comprehension fib P
open Comonad-on
+ open is-comonad
```
We begin by constructing the endofunctor $\int E \to \int E$, which maps
@@ -470,12 +471,9 @@ is given by duplication.
∫hom δᶜ δᶜ'
comonad .comult .is-natural (Γ , x) (Δ , g) (∫hom σ f) =
∫Hom-path E dup-extend dup-extend'
- comonad .δ-unitl =
- ∫Hom-path E extend-proj-dup extend-proj-dup'
- comonad .δ-unitr =
- ∫Hom-path E proj-dup proj-dup'
- comonad .δ-assoc =
- ∫Hom-path E extend-dup² extend-dup²'
+ comonad .has-is-comonad .δ-unitl = ∫Hom-path E extend-proj-dup extend-proj-dup'
+ comonad .has-is-comonad .δ-unitr = ∫Hom-path E proj-dup proj-dup'
+ comonad .has-is-comonad .δ-assoc = ∫Hom-path E extend-dup² extend-dup²'
```
To see that this comonad is a comprehension comonad, note that the
diff --git a/src/Cat/Displayed/Instances/Factorisations.lagda.md b/src/Cat/Displayed/Instances/Factorisations.lagda.md
new file mode 100644
index 000000000..f7a0f1e15
--- /dev/null
+++ b/src/Cat/Displayed/Instances/Factorisations.lagda.md
@@ -0,0 +1,414 @@
+
+
+```agda
+module Cat.Displayed.Instances.Factorisations where
+```
+
+
+
+
+
+# The displayed category of factorisations
+
+Given a category $\cC$, we can define a [[displayed category]] $\cC^3
+\liesover \operatorname{Arr}(\cC)$ over the [[arrow category]]
+$\Arr{\cC}$ where an object over $f : X \to Y$ consists of a
+factorisation
+$$
+X \xto{f} Y = X \xto{m} I \xto{e} Y
+$$
+of $f$ through some choice of object $M$. This is akin to the
+non-displayed notion of [factorisation], but without the reference to
+pre-existing classes $M$ and $E$ for $m$ and $e$ to belong to.
+
+[factorisation]: Cat.Morphism.Factorisation.html
+
+```agda
+ record Splitting {X Y : ⌞ C ⌟} (f : Hom X Y) : Type (o ⊔ ℓ) where
+ no-eta-equality
+ field
+ {mid} : ⌞ C ⌟
+ left : Hom X mid
+ right : Hom mid Y
+ factors : f ≡ right ∘ left
+```
+
+
+
+A morphism between splittings lying over a square from $f$ to $g$ in the
+arrow category, depicted in blue in the diagram below, is a map $i : I
+\to I'$ between the "middle" objects of the two factorisations making
+both the top and bottom rectangles commute.
+
+~~~{.quiver .attach-around}
+\[\begin{tikzcd}[ampersand replacement=\&]
+ \textcolor{rgb,255:red,92;green,92;blue,214}{X} \&\& \textcolor{rgb,255:red,92;green,92;blue,214}{{X'}} \\
+ I \&\& {I'} \\
+ \textcolor{rgb,255:red,92;green,92;blue,214}{Y} \&\& \textcolor{rgb,255:red,92;green,92;blue,214}{{Y'}}
+ \arrow["t", color={rgb,255:red,92;green,92;blue,214}, from=1-1, to=1-3]
+ \arrow["m", from=1-1, to=2-1]
+ \arrow["f"', color={rgb,255:red,92;green,92;blue,214}, curve={height=12pt}, from=1-1, to=3-1]
+ \arrow["{m'}"', from=1-3, to=2-3]
+ \arrow["g", color={rgb,255:red,92;green,92;blue,214}, curve={height=-12pt}, from=1-3, to=3-3]
+ \arrow["i"{description}, dashed, from=2-1, to=2-3]
+ \arrow["o", from=2-1, to=3-1]
+ \arrow["{o'}"', from=2-3, to=3-3]
+ \arrow["b"', color={rgb,255:red,92;green,92;blue,214}, from=3-1, to=3-3]
+\end{tikzcd}\]
+~~~
+
+```agda
+ record
+ Interpolant
+ {X X' Y Y'} {f : Hom X Y} {g : Hom X' Y'}
+ (sq : Homᵃ C f g) (s : Splitting f) (t : Splitting g)
+ : Type ℓ where
+```
+
+
+
+```agda
+ field
+ map : Hom (s .mid) (t .mid)
+ 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
+this displayed category is identified with the diagram category $\cC^3$
+of composable *triples*[^three] in $\cC$, and its projection functor
+$\cC^3 \to \Arr{\cC}$ sends each triple to its composite. In a proof
+assistant, defining this as a displayed category is superior because it
+lets us define [[*sections*|section of a displayed category]] of the
+composition functor--- which send each arrow to a factorisation--- where
+the domain and codomain of a factored arrow are *definitionally* the
+ones we started with.
+
+[^three]:
+ Note that here $3$ denotes the *ordinal* $\{0 \le 1 \le 2\}$,
+ and not the set with three elements.
+
+
+
+```agda
+ Factorisations' : Displayed (Arr C) _ _
+ Factorisations' .Ob[_] (_ , _ , f) = Splitting C f
+ Factorisations' .Hom[_] sq s s' = Interpolant C sq s s'
+
+ Factorisations' .id' = record { sq₀ = id-comm ; sq₁ = id-comm }
+
+ Factorisations' ._∘'_ f g = record where
+ map = f .map ∘ g .map
+ sq₀ = pulll (f .sq₀) ∙ extendr (g .sq₀)
+ sq₁ = pulll (f .sq₁) ∙ extendr (g .sq₁)
+```
+
+
+The only interesting to note about the coherence data here is
+that we can reindex `Interpolant`{.Agda}s over identifications between
+squares without disturbing the middle map.
+
+```agda
+ Factorisations' .Hom[_]-set f x y = hlevel 2
+
+ Factorisations' .idr' f = Interpolant-pathp (idr _)
+ Factorisations' .idl' f = Interpolant-pathp (idl _)
+ Factorisations' .assoc' f g h = Interpolant-pathp (assoc _ _ _)
+
+ Factorisations' .hom[_] p' f = record where
+ map = f .map
+ sq₀ = ap₂ _∘_ refl (sym (ap top p')) ∙ f .sq₀
+ sq₁ = f .sq₁ ∙ ap₂ _∘_ (ap bot p') refl
+ Factorisations' .coh[_] p' f = Interpolant-pathp refl
+```
+
+
+
+# Functorial factorisations
+
+::: {.definition #functorial-factorisation}
+A **(functorial) factorisation** on $\cC$ is a [[section|section of a
+displayed category]] of `Factorisations'`{.Agda}. These naturally
+assemble into a category.
+:::
+
+```agda
+ Factorisation : Type _
+ Factorisation = Section Factorisations'
+
+ Factorisations : Precategory _ _
+ Factorisations = Sections Factorisations'
+```
+
+We shall now identify some first properties of functorial
+factorisations.
+
+
+
+
+Because the morphism-assignment of sections has a pretty
+dependent type, we can not immediately reuse the functor reasoning
+combinators for functorial factorisations.
+
+Adapting them to this case is pretty straightforward, though, so here
+are the ones we'll need.
+
+
+```agda
+ adjust
+ : ∀ {u v w x} {f : Hom u v} {g : Hom w x} {sq sq' : Homᵃ C f g}
+ → sq ≡ sq'
+ → S₁ sq .map ≡ S₁ sq' .map
+ adjust p = apd (λ i → map) (ap S₁ p)
+
+ weave
+ : ∀ {u v w x w' x' y z} {f : Hom u v} {g : Hom w x} {g' : Hom w' x'} {h : Hom y z}
+ → {sq : Homᵃ C g h} {sq' : Homᵃ C f g}
+ → {tq : Homᵃ C g' h} {tq' : Homᵃ C f g'}
+ → sq Arr.∘ sq' ≡ tq Arr.∘ tq'
+ → S₁ sq .map ∘ S₁ sq' .map
+ ≡ S₁ tq .map ∘ S₁ tq' .map
+ weave p = apd (λ i → map) (sym (S-∘ _ _)) ∙∙ adjust p ∙∙ apd (λ i → map) (S-∘ _ _)
+
+ collapse
+ : ∀ {u v w x y z} {f : Hom u v} {g : Hom w x} {h : Hom y z}
+ → {sq : Homᵃ C g h} {sq' : Homᵃ C f g} {tq : Homᵃ C f h}
+ → sq Arr.∘ sq' ≡ tq
+ → S₁ sq .map ∘ S₁ sq' .map
+ ≡ S₁ tq .map
+ collapse p = apd (λ i → map) (sym (S-∘ _ _)) ∙ adjust p
+
+ expand
+ : ∀ {u v w x y z} {f : Hom u v} {g : Hom w x} {h : Hom y z}
+ → {sq : Homᵃ C g h} {sq' : Homᵃ C f g} {tq : Homᵃ C f h}
+ → tq ≡ sq Arr.∘ sq'
+ → S₁ tq .map
+ ≡ S₁ sq .map ∘ S₁ sq' .map
+ expand p = sym (collapse (sym p))
+
+ annihilate : ∀ {u v} {f : Hom u v} {sq : Homᵃ C f f} → sq ≡ Arr.id → S₁ sq .map ≡ id
+ annihilate p = adjust p ∙ apd (λ i → map) S-id
+```
+
+
+
+Given a functorial factorisation, we can define two endofunctors on
+$\Arr{\cC}$, referred to simply as its *left* and *right* parts, which
+send a morphism $X \xto{f} Y$ to $L(f) = X \xto{m} I(f)$ and $R(f) =
+I(f) \xto{o} Y$, respectively, while sending a square to either the top
+or bottom rectangles in the definition of `Interpolant`{.Agda}.
+
+::: commented-out
+
+:::{.definition #left-factor-functor}
+If $F$ is a [[functorial factorisation]] on $\cC$, splitting an $X
+\xto{f} Y$ into $X \xto{\lambda} M \xto{\rho} Y$ the **left factor
+functor** on $\Arr{\cC}$ is $L(f) = X \xto{\lambda} M$. This is
+naturally made into a *copointed endofunctor*, with the counit assigning
+to each arrow $X \xto{f} Y$ the square
+
+~~~{.quiver .attach-above}
+\[\begin{tikzcd}[ampersand replacement=\&]
+ X \&\& X \\
+ \\
+ M \&\& {Y\text{.}}
+ \arrow[equals, from=1-1, to=1-3]
+ \arrow["\lambda"', from=1-1, to=3-1]
+ \arrow["f", from=1-3, to=3-3]
+ \arrow["\rho"', from=3-1, to=3-3]
+\end{tikzcd}\]
+~~~
+:::
+
+:::{.definition #right-factor-functor}
+If $F$ is a [[functorial factorisation]] on $\cC$, splitting an $X
+\xto{f} Y$ into $X \xto{\lambda} M \xto{\rho} Y$ the **right factor
+functor** on $\Arr{\cC}$ is $R(f) = M \xto{\rho} Y$. This is naturally
+made into a *pointed endofunctor*, with the unit assigning to each arrow
+$X \xto{f} Y$ the square
+
+~~~{.quiver .attach-above}
+\[\begin{tikzcd}[ampersand replacement=\&]
+ M \&\& X \\
+ \\
+ Y \&\& {Y\text{.}}
+ \arrow["\lambda", from=1-1, to=1-3]
+ \arrow["\rho"', from=1-1, to=3-1]
+ \arrow["f", from=1-3, to=3-3]
+ \arrow[equals, from=3-1, to=3-3]
+\end{tikzcd}\]
+~~~
+:::
+
+:::
+
+```agda
+ L : Functor (Arr C) (Arr C)
+ L .F₀ (X , Y , f) = X , Mid f , λ→ f
+ L .F₁ {X , Z , f} {X' , Z' , f'} sq = record
+ { top = sq .top
+ ; bot = S₁ sq .map
+ ; com = S₁ sq .sq₀
+ }
+ L .F-id = ext (refl ,ₚ annihilate refl)
+ L .F-∘ f g = ext (refl ,ₚ expand refl)
+
+ R : Functor (Arr C) (Arr C)
+ R .F₀ (X , Y , f) = Mid f , Y , ρ→ f
+ R .F₁ {X , Z , f} {X' , Z' , f'} sq = record
+ { top = S₁ sq .map
+ ; bot = sq .bot
+ ; com = S₁ sq .sq₁
+ }
+ R .F-id = ext (annihilate refl ,ₚ refl)
+ R .F-∘ f g = ext (expand refl ,ₚ refl)
+```
+
+
+
+These endofunctors are naturally *(co)pointed*, meaning that the left
+(resp. right) functor admits a natural transformation *to* (resp.
+*from*) the identity on $\Arr{\cC}$. These transformations send a
+morphism to a triangle consisting of the complementary part of the
+factorisation.
+
+```agda
+ L-ε : L => Id
+ L-ε .η (X , Y , f) = record
+ { top = id
+ ; bot = ρ→ f
+ ; com = elimr refl ∙ factors f
+ }
+ L-ε .is-natural x y f = ext (id-comm-sym ,ₚ S₁ f .sq₁)
+
+ R-η : Id => R
+ R-η .η (X , Y , f) = record
+ { top = λ→ f
+ ; bot = id
+ ; com = sym (factors f) ∙ introl refl
+ }
+ R-η .is-natural x y f = ext (S₁ f .sq₀ ,ₚ id-comm-sym)
+```
+
+
diff --git a/src/Cat/Displayed/Section.lagda.md b/src/Cat/Displayed/Section.lagda.md
index ed27204ba..5f0f6cd73 100644
--- a/src/Cat/Displayed/Section.lagda.md
+++ b/src/Cat/Displayed/Section.lagda.md
@@ -38,6 +38,7 @@ arguments.
```agda
record Section : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
+ no-eta-equality
field
S₀ : (x : ⌞ B ⌟) → E ʻ x
S₁ : {x y : ⌞ B ⌟} (f : B.Hom x y) → E.Hom[ f ] (S₀ x) (S₀ y)
diff --git a/src/Cat/Functor/Adjoint/Comonad.lagda.md b/src/Cat/Functor/Adjoint/Comonad.lagda.md
index 5c79bcae5..f4d85acf3 100644
--- a/src/Cat/Functor/Adjoint/Comonad.lagda.md
+++ b/src/Cat/Functor/Adjoint/Comonad.lagda.md
@@ -8,6 +8,7 @@ open import Cat.Functor.Adjoint
open import Cat.Prelude
open Comonad-on
+open is-comonad
open Functor
open _=>_
```
@@ -62,13 +63,13 @@ right identity law is exactly the `zig`{.Agda ident="adj.zag"}
identity.
```agda
-Adjunction→Comonad .δ-unitr {x} = adj.zig
+Adjunction→Comonad .has-is-comonad .δ-unitr {x} = adj.zig
```
The others are slightly more involved.
```agda
-Adjunction→Comonad .δ-unitl {x} = path where abstract
+Adjunction→Comonad .has-is-comonad .δ-unitl {x} = path where abstract
path : L.₁ (R.₁ (adj.ε x)) D.∘ L.₁ (adj.η (R.F₀ x)) ≡ D.id
path =
L.₁ (R.₁ (adj.ε _)) D.∘ L.₁ (adj.η _) ≡⟨ sym (L.F-∘ _ _) ⟩
@@ -76,7 +77,7 @@ Adjunction→Comonad .δ-unitl {x} = path where abstract
L.₁ C.id ≡⟨ L.F-id ⟩
D.id ∎
-Adjunction→Comonad .δ-assoc {x} = path where abstract
+Adjunction→Comonad .has-is-comonad .δ-assoc {x} = path where abstract
path : L.₁ (R.₁ (L.₁ (adj.η (R.F₀ x)))) D.∘ L.₁ (adj.η _)
≡ L.₁ (adj.η (R .F₀ (L.F₀ (R.F₀ x)))) D.∘ L.₁ (adj.η _)
path =
diff --git a/src/Cat/Functor/Adjoint/Monad.lagda.md b/src/Cat/Functor/Adjoint/Monad.lagda.md
index 4d4608320..01d4ea515 100644
--- a/src/Cat/Functor/Adjoint/Monad.lagda.md
+++ b/src/Cat/Functor/Adjoint/Monad.lagda.md
@@ -8,6 +8,7 @@ open import Cat.Diagram.Monad
open import Cat.Prelude
open Monad-on
+open is-monad
open Functor
open _=>_
```
@@ -61,13 +62,13 @@ left identity law is exactly the `zag`{.Agda ident="adj.zag"}
identity.
```agda
-Adjunction→Monad .μ-unitl {x} = adj.zag
+Adjunction→Monad .has-is-monad .μ-unitl {x} = adj.zag
```
The others are slightly more involved.
```agda
-Adjunction→Monad .μ-unitr {x} = path where abstract
+Adjunction→Monad .has-is-monad .μ-unitr {x} = path where abstract
path : R.₁ (adj.ε (L.F₀ x)) C.∘ R.₁ (L.₁ (adj.η x)) ≡ C.id
path =
R.₁ (adj.ε _) C.∘ R.₁ (L.₁ (adj.η _)) ≡⟨ sym (R.F-∘ _ _) ⟩
@@ -75,7 +76,7 @@ Adjunction→Monad .μ-unitr {x} = path where abstract
R.₁ D.id ≡⟨ R.F-id ⟩
C.id ∎
-Adjunction→Monad .μ-assoc {x} = path where abstract
+Adjunction→Monad .has-is-monad .μ-assoc {x} = path where abstract
path : R.₁ (adj.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.ε (L.F₀ x))))
≡ R.₁ (adj.ε _) C.∘ R.₁ (adj.ε (L .F₀ (R.F₀ (L.F₀ x))))
path =
diff --git a/src/Cat/Instances/Shape/Interval.lagda.md b/src/Cat/Instances/Shape/Interval.lagda.md
index f45c01664..4872c0dc8 100644
--- a/src/Cat/Instances/Shape/Interval.lagda.md
+++ b/src/Cat/Instances/Shape/Interval.lagda.md
@@ -92,7 +92,7 @@ function.
0≤1-products A B .has-is-product .unique _ _ = prop!
```
-# The space of arrows
+# The space of arrows {defines="arrow-category"}
The total space of the $\hom$ family of a precategory is referred to as
its "space of arrows". A point in this space is a "free-standing arrow":
@@ -234,7 +234,9 @@ module _ {o ℓ} {C : Precategory o ℓ} {a b x y : ⌞ C ⌟} {f : C .Hom a b}
→ Extensional (Homᵃ C f g) ℓr
Extensional-Homᵃ ⦃ sab ⦄ =
injection→extensional!
- (λ p → Iso.injective eqv (Σ-pathp (ap fst p) (Σ-pathp (ap snd p) prop!)))
+ (λ { p i .top → p i .fst
+ ; p i .bot → p i .snd
+ ; {x} {y} p i .com → is-prop→pathp (λ i → C .Hom-set _ _ (C ._∘_ g (p i .fst)) (C ._∘_ (p i .snd) f)) (x .com) (y .com) i })
sab
```
-->
diff --git a/src/Cat/Monoidal/Instances/Factorisations.lagda.md b/src/Cat/Monoidal/Instances/Factorisations.lagda.md
new file mode 100644
index 000000000..1ede17383
--- /dev/null
+++ b/src/Cat/Monoidal/Instances/Factorisations.lagda.md
@@ -0,0 +1,348 @@
+
+
+```agda
+module Cat.Monoidal.Instances.Factorisations {o ℓ} (C : Precategory o ℓ) where
+```
+
+
+
+# Monoidal structure on functorial factorisations
+
+We show how to equip the category $\Ff{\cC}$ of [[functorial
+factorisations]] on $\cC$ with the structure of a [[monoidal category]],
+such that a [monoid] on some factorisation $F : \Ff{\cC}$ is precisely a
+[[right weak factorisation structure]] on $\cC$.
+
+[monoid]: Cat.Monoidal.Diagram.Monoid.html
+
+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
+ { left = id
+ ; right = f
+ ; factors = intror refl
+ }
+Ff-unit .S₁ f = record
+ { sq₀ = id-comm-sym
+ ; sq₁ = f .com
+ }
+Ff-unit .S-id = ext refl
+Ff-unit .S-∘ f g = ext refl
+```
+
+
+
+We can easily calculate that the this unit factorisation is [[initial]].
+
+```agda
+Ff-unit-is-initial : is-initial (Factorisations C) Ff-unit
+```
+
+
+```agda
+Ff-unit-is-initial other = record where
+ module o = Factorisation other
+ centre = record
+ { map = λ (X , Y , f) → record
+ { map = o.λ→ f
+ ; sq₀ = refl
+ ; sq₁ = sym (o.factors f) ∙ introl refl
+ }
+ ; com = λ x y f → Interpolant-pathp (other .S₁ f .sq₀)
+ }
+ paths h = ext λ x y f →
+ o.λ→ f ≡⟨ h .sq₀ᶠᶠ f ⟩
+ h .mapᶠᶠ f ∘ id ≡⟨ elimr refl ⟩
+ h .mapᶠᶠ f ∎
+```
+
+
+
+If $F, F' : \Ff{\cC}$ are a pair of factorisations, their tensor $F
+\otimes F'$ sends a map $X \xto{F} Y$ to the composite
+$$
+X \xto{\lambda_f} M(f) \xto{\lambda'_{\rho_f}} M'(\rho_f) \xto{\rho'_{\rho_f}} Y
+$$
+with "middle object" $M'(\rho_f)$, i.e. everything but the last arrow is
+the left factor.
+
+```agda
+module _ (F G : Factorisation C) where
+ private
+ module F = Factorisation F
+ module G = Factorisation G
+
+ _⊗ᶠᶠ_ : Factorisation C
+ _⊗ᶠᶠ_ .S₀ (_ , _ , f) = record where
+ 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₁ })
+ using (sq₁ ; map)
+ renaming (sq₀ to α)
+
+ sq₀ = sym (pulll (sym α) ∙ extendr (sym (F .S₁ sq .sq₀)))
+
+ _⊗ᶠᶠ_ .S-id = ext (G.annihilate (ext (F.annihilate refl ,ₚ refl)))
+ _⊗ᶠᶠ_ .S-∘ f g = ext (G.expand (ext (F.expand refl ,ₚ refl)))
+```
+
+
+Showing that this extends to a functor is slightly annoying,
+but unsurprising.
+
+```agda
+Ff-tensor-functor : Functor (Ff ×ᶜ Ff) Ff
+Ff-tensor-functor .F₀ (F , F') = F ⊗ᶠᶠ F'
+Ff-tensor-functor .F₁ {X , Y} {X' , Y'} (f , g) .map (_ , _ , h) =
+ let
+ sq = record { com = f .sq₁ᶠᶠ h ∙ introl refl }
+ h' = g .map (_ , _ , Factorisation.ρ→ X h)
+ in record
+ { map = Y' .S₁ sq .map ∘ h' .map
+ ; sq₀ = sym
+ ( pullr (pulll (sym (h' .sq₀)))
+ ∙∙ pulll (pulll (sym (Y' .S₁ sq .sq₀)) ∙ elimr refl)
+ ∙∙ pullr (sym (f .sq₀ᶠᶠ h))
+ ∙ intror refl)
+ ; sq₁ = pulll (Y' .S₁ sq .sq₁)
+ ∙ pullr (h' .sq₁ ∙ eliml refl)
+ }
+
+Ff-tensor-functor .F₁ {X , Y} {X' , Y'} (f , g) .com α β h = Interpolant-pathp $
+ pullr (g .comᶠᶠ _)
+ ∙ extendl (weave Y' (ext (f .comᶠᶠ _ ,ₚ id-comm-sym)))
+
+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)))))
+```
+
+
+
+The following snippet, showing part of the construction of the
+associator, is typical of the construction of the monoidal structure on
+$\Ff{\cC}$: every *component* of the natural isomorphisms is the
+identity, but we end up having to shuffle quite a few identity morphisms
+around.
+
+```agda
+private
+ assc : Associator-for {O = ⊤} (λ _ _ → Ff) Ff-tensor-functor
+ assc = to-natural-iso mk where
+ mk : make-natural-iso (compose-assocˡ Ff-tensor-functor) _
+ mk .eta X .map x = record
+ { map = id
+ ; sq₀ = elimr refl ∙∙ pullr refl ∙∙ introl refl
+ ; sq₁ = id-comm
+ }
+ mk .inv X .map x = record
+ { map = id
+ ; sq₀ = elimr refl ∙∙ pulll refl ∙∙ introl refl
+ ; sq₁ = id-comm
+ }
+```
+
+
+
+
+
+```agda
+Ff-monoidal : Monoidal-category Ff
+Ff-monoidal .-⊗- = Ff-tensor-functor
+Ff-monoidal .Unit = Ff-unit
+```
+
+We thus choose not to comment much on the construction of the unitors
+and proof of the triangle and pentagon identities.
+
+
+```agda
+Ff-monoidal .unitor-l = to-natural-iso mk where
+ mk : make-natural-iso (Id {C = Ff}) (Bi.Right Ff-tensor-functor Ff-unit)
+ mk .eta X .map _ = record { sq₀ = cancelr (idl id) ∙ introl refl ; sq₁ = id-comm }
+ mk .inv X .map _ = record { sq₀ = introl refl ; sq₁ = id-comm }
+
+ mk .eta X .com x y f = Interpolant-pathp $
+ eliml refl ∙∙ adjust X (ext refl) ∙∙ intror refl
+ mk .inv X .com x y f = Interpolant-pathp $
+ eliml refl ∙∙ adjust X (ext refl) ∙∙ intror refl
+
+ mk .eta∘inv x = ext λ x y f → idl id
+ mk .inv∘eta x = ext λ x y f → idl id
+ mk .natural X Y f = ext λ x y g →
+ elimr refl ∙∙ eliml (annihilate Y (ext refl)) ∙∙ introl refl
+
+Ff-monoidal .unitor-r = to-natural-iso mk where
+ mk : make-natural-iso (Id {C = Ff}) (Bi.Left Ff-tensor-functor Ff-unit)
+ mk .eta X .map _ = record { sq₀ = elimr refl ; sq₁ = id-comm }
+ mk .inv X .map _ = record { sq₀ = elimr refl ∙ insertl (idl id) ; sq₁ = id-comm }
+
+ mk .eta X .com x y f = Interpolant-pathp $
+ eliml refl ∙∙ Factorisation.adjust X (ext refl) ∙∙ intror refl
+ mk .inv X .com x y f = Interpolant-pathp $
+ eliml refl ∙∙ Factorisation.adjust X (ext refl) ∙∙ intror refl
+
+ mk .eta∘inv x = ext λ x y f → idl id
+ mk .inv∘eta x = ext λ x y f → idl id
+ mk .natural X Y f = ext λ x y g → cancelr (idl id) ∙ introl refl
+
+Ff-monoidal .associator = assc
+Ff-monoidal .triangle = ext λ x y f → pullr (idl id)
+Ff-monoidal .pentagon {B = B} {C = C} {D = D} = ext λ x y f →
+ pullr
+ ( cancell (idl id)
+ ∙∙ elimr refl
+ ∙∙ annihilate D (ext (annihilate C (ext (annihilate B (ext refl) ,ₚ refl)) ,ₚ refl)))
+ ∙ ap (_∘ id) (annihilate D (ext refl))
+```
+
+
+
+# Monoids on functorial factorisations
+
+
+
+We will now show that a monoid (on some functorial factorisation $F :
+\Ff{\cC}$) in this monoidal structure can be tweaked into a [[right weak
+factorisation structure]] on $F$. First, note that the components of the
+monoidal multiplication on $F$ can be reassembled into a *monadic*
+multiplication on the right factor.
+
+```agda
+ private
+ monoid→mult : F.R F∘ F.R => F.R
+ monoid→mult .η (X , Y , f) = record where
+ top = m.μ .mapᶠᶠ f
+ bot = id
+ com = m.μ .sq₁ᶠᶠ f ∙ introl refl
+ monoid→mult .is-natural x y f = ext $
+ ap₂ _∘_ refl (F.adjust (ext refl)) ∙ m.μ .comᶠᶠ _ ,ₚ
+ id-comm-sym
+```
+
+
+For ease of calculation below, we can also extract a *unit* map
+from the monoid structure on $F$.
+
+```agda
+ monoid→unit : Id => F.R
+ monoid-unit-agrees : monoid→unit ≡ F.R-η
+```
+
+Of course, what we need to show is that the monoid multiplication makes
+the [[right factor functor]] $R$, *with its canonical unit* $\eta$, into
+a monad. However, that the unit derived from the monoid agrees with
+$\eta$ is an easy corollary of initiality for the unit factorisation.
+
+
+```agda
+ monoid→unit .η (X , Y , f) = record
+ { top = m.η .mapᶠᶠ f
+ ; bot = id
+ ; com = m.η .sq₁ᶠᶠ f ∙ introl refl
+ }
+ 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
+```
+
+
+
+The calculation that these two are a monad on $R$ is a straightforward
+repackaging of the corresponding monoid laws.
+
+```agda
+ monoid-mult-is-monad : is-monad monoid→unit monoid→mult
+ monoid-mult-is-monad .μ-unitr {X , Y , f} = ext $
+ ap₂ _∘_ refl (F.adjust (ext refl) ∙ intror refl)
+ ∙ apd (λ i x → x .mapᶠᶠ f) m.μ-unitl
+ ,ₚ idl id
+
+ monoid-mult-is-monad .μ-unitl {X , Y , f} = ext $
+ ap₂ _∘_ refl (introl (F.annihilate (ext refl)))
+ ∙ apd (λ i x → x .mapᶠᶠ f) m.μ-unitr
+ ,ₚ idl id
+
+ monoid-mult-is-monad .μ-assoc {X , Y , f} = ext $
+ ap₂ _∘_ refl (F.adjust (ext (refl ,ₚ refl)) ∙∙ intror refl ∙∙ intror refl)
+ ∙∙ apd (λ i x → x .mapᶠᶠ f) (sym m.μ-assoc)
+ ∙∙ ap₂ _∘_ refl (eliml (F.annihilate (ext refl)))
+ ,ₚ refl
+```
+
+We can then transport this along the proof that the units agree to
+extend $(R, \eta)$ to a monad. This transport will not compute very
+nicely, but since "being a monad" is a proposition once the unit and
+multiplication are fixed, this does not matter.
+
+```agda
+ monoid-on→rwfs-on : Rwfs-on F
+ 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
+ monoid-mult-is-monad
+```
diff --git a/src/Cat/Monoidal/Instances/Factorisations/Left.lagda.md b/src/Cat/Monoidal/Instances/Factorisations/Left.lagda.md
new file mode 100644
index 000000000..f4aeaeb37
--- /dev/null
+++ b/src/Cat/Monoidal/Instances/Factorisations/Left.lagda.md
@@ -0,0 +1,184 @@
+
+
+```agda
+module Cat.Monoidal.Instances.Factorisations.Left
+ {o ℓ} (C : Precategory o ℓ) where
+```
+
+
+
+# Monoidal structure on lwfs
+
+The [[monoidal category]] [structure] on [[functorial factorisations]]
+lifts to [[left weak factorisation structures]].
+
+[structure]: Cat.Monoidal.Instances.Factorisations.html
+
+The comultiplication on the tensor unit is trivial.
+
+```agda
+Lwfs-on-unit : Lwfs-on Ff-unit
+Lwfs-on-unit .L-δ .η (X , Y , f) = Arr.id
+Lwfs-on-unit .L-δ .is-natural x y f = ext (id-comm-sym ,ₚ id-comm-sym)
+Lwfs-on-unit .L-comonad .δ-unitl = ext (idl id ,ₚ idl id)
+Lwfs-on-unit .L-comonad .δ-unitr = ext (idl id ,ₚ idl id)
+Lwfs-on-unit .L-comonad .δ-assoc = ext refl
+```
+
+The comultiplication on tensors is where most of the work goes.
+
+```agda
+module _ {F G : Factorisation C} (Fl : Lwfs-on F) (Gl : Lwfs-on G) where
+```
+
+
+
+```agda
+ λλ : ∀ {x y} (f : Hom x y) → Hom x (G.Mid (ρᶠ f))
+ λλ f = λᵍ (ρᶠ f) ∘ λᶠ f
+
+ λ→λλ : ∀ {x y} (f : Hom x y) → Homᵃ C (λᶠ f) (λλ f)
+ λ→λλ f .top = id
+ λ→λλ f .bot = λᵍ (ρᶠ f)
+ λ→λλ f .com = elimr refl
+```
+
+```agda
+ δ-sq : ∀ {x y} (f : Hom x y) → Homᵃ C (λᵍ (ρᶠ f)) (ρᶠ (λλ f))
+ δ-sq f using (llift , α , β) ← F.lift-λρ (λ→λλ f) = record
+ { top = llift
+ ; bot = id
+ ; com = β ∙ introl refl
+ }
+```
+
+The component of the comultiplication $\delta$ at a map $X \xto{f} Y$ is
+given by the dashed arrow $l_2$ in the diagram below. The auxiliary
+arrow $l_1$ serves primarily to establish that everything necessary
+commutes. Note that the ellipse with faces $\rho_{\rho_{\dots}}$ and
+$l_2$ is only the identity on $G(\rho_f)$, and this gives one of the
+counit laws for $\delta$.
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+ \& X \\
+ \\
+ Y \& {F(f)} \& {F(\lambda^2_f)} \\
+ \\
+ \& {G(\rho_f)} \&\& {G(\rho_{\lambda^2_f})}
+ \arrow["f"', dotted, from=1-2, to=3-1]
+ \arrow["{\lambda_f}", from=1-2, to=3-2]
+ \arrow["{\lambda_{\lambda^2_f}}", from=1-2, to=3-3]
+ \arrow["{l_1}", dashed, from=3-2, to=3-3]
+ \arrow["{\lambda_{\rho_f}}"', from=3-2, to=5-2]
+ \arrow["{\rho_{\lambda^2_f}}"', dotted, from=3-3, to=5-2]
+ \arrow["{\lambda_{\rho_{\lambda^2_f}}}", from=3-3, to=5-4]
+ \arrow["{\rho_{\lambda_f}}", dotted, from=5-2, to=3-1]
+ \arrow["{l_2}"', dashed, from=5-2, to=5-4]
+ \arrow["{\rho_{\rho_{\lambda^2_f}}}"', curve={height=24pt}, from=5-4, to=5-2]
+\end{tikzcd}\]
+~~~
+
+```agda
+ lδ : FG.L => (FG.L F∘ FG.L)
+ lδ .η (X , Y , f) = record where
+ (l1 , α , _) = F.lift-λρ (λ→λλ f)
+ (bot , β , _) = G.lift-λρ (δ-sq f)
+
+ top = id
+ com : (λᵍ (ρᶠ (λλ f)) ∘ λᶠ (λλ f)) ∘ id ≡ bot ∘ λᵍ (ρᶠ f) ∘ λᶠ f
+ com = sym (pulll β ∙∙ pullr α ∙∙ pulll refl)
+```
+
+
+
+As indicated, we can obtain one of the counit laws by pondering the orb
+contained in the diagram, and the other counit law pops up by
+calculating until we can apply $F$ and $G$'s unit laws in turn. The only
+lengthy calculation is associativity, but the idea is the same:
+calculate to expose opportunities to apply the associativity of both
+factors.
+
+```agda
+ Lwfs-on-tensor : Lwfs-on (F ⊗ᶠᶠ G)
+ Lwfs-on-tensor .L-δ = lδ
+ Lwfs-on-tensor .L-comonad .δ-assoc {x , y , f} = ext $ refl ,ₚ sym p1 where
+ p0 =
+ F.map (λ→λλ (λλ f)) ∘ F.δ (λλ f) ∘ F.map (λ→λλ f) ∘ F.δ f
+ ≡⟨ ap₂ _∘_ refl (pulll (sym (F.δ-nat _)) ∙ pullr (sym F.δ-assoc)) ⟩
+ F.map (λ→λλ (λλ f)) ∘ F.map (F.L₁ (λ→λλ f)) ∘ F.map (F.δˢ f) ∘ F.δ f
+ ≡⟨ pulll (F.collapse refl) ⟩
+ F.map (λ→λλ (λλ f) Arr.∘ F.L₁ (λ→λλ f)) ∘ F.map (F.δˢ f) ∘ F.δ f
+ ≡⟨ extendl (F.weave (ext (elimr F.δ-top ,ₚ pullr refl ∙ sym (G.lift-λρ (δ-sq f) .snd .fst)))) ⟩
+ F.map (lδ .η (_ , _ , f)) ∘ F.map (λ→λλ f) ∘ F.δ f
+ ∎
+
+ p1 =
+ (G.map (δ-sq (λλ f)) ∘ G.δ (ρᶠ (λλ f))) ∘ G.map (δ-sq f) ∘ G.δ (ρᶠ f)
+ ≡⟨ pullr (extendl (sym (G.δ-nat _))) ⟩
+ G.map (δ-sq (λλ f)) ∘ G.map (G.L₁ (δ-sq f)) ∘ G.δ (λᵍ (ρᶠ f)) ∘ G.δ (ρᶠ f)
+ ≡⟨ ap₂ _∘_ refl (ap₂ _∘_ refl (sym G.δ-assoc)) ⟩
+ G.map (δ-sq (λλ f)) ∘ G.map (G.L₁ (δ-sq f)) ∘ G.map (G.δˢ (ρᶠ f)) ∘ G.δ (ρᶠ f)
+ ≡⟨ ap₂ _∘_ refl (pulll (G.collapse refl)) ⟩
+ G.map (δ-sq (λλ f)) ∘ G.map (G.L₁ (δ-sq f) Arr.∘ G.δˢ (ρᶠ f)) ∘ G.δ (ρᶠ f)
+ ≡⟨ extendl (G.weave (ext (pullr (ap₂ _∘_ refl (elimr G.δ-top)) ∙ p0 ,ₚ pulll (eliml refl) ∙ intror refl))) ⟩
+ G.map _ ∘ G.map (δ-sq f) ∘ G.δ (ρᶠ f)
+ ∎
+```
+
+
diff --git a/src/Cat/Morphism/Factorisation/Algebraic.lagda.md b/src/Cat/Morphism/Factorisation/Algebraic.lagda.md
new file mode 100644
index 000000000..1e9c8bf75
--- /dev/null
+++ b/src/Cat/Morphism/Factorisation/Algebraic.lagda.md
@@ -0,0 +1,167 @@
+
+
+```agda
+module Cat.Morphism.Factorisation.Algebraic where
+```
+
+# Algebraic weak factorisation systems
+
+
+
+:::{.definition #left-weak-factorisation-structure}
+A **left weak factorisation structure** on a [[functorial
+factorisation]] $F$ is an extension of the [[left factor functor]] $(L,
+\eps)$ into a [[comonad]] on $\Arr{\cC}$.
+:::
+
+```agda
+ record Lwfs-on : Type (o ⊔ ℓ) where
+ field
+ L-δ : L => L F∘ L
+ L-comonad : is-comonad L-ε L-δ
+
+ open is-comonad L-comonad using (ε ; δ ; δ-unitl ; δ-unitr ; δ-assoc ; module counit ; module comult) public
+
+ 𝕃 : Comonad-on L
+ 𝕃 = record { has-is-comonad = L-comonad }
+```
+
+:::{.definition #right-weak-factorisation-structure}
+A **right weak factorisation structure** on a [[functorial
+factorisation]] $F$ is an extension of the [[right factor functor]] $(R,
+\eta)$ into a [[monad]] on $\Arr{\cC}$.
+:::
+
+```agda
+ record Rwfs-on : Type (o ⊔ ℓ) where
+ field
+ R-μ : R F∘ R => R
+ R-monad : is-monad R-η R-μ
+
+ open is-monad R-monad using (η ; μ ; μ-unitl ; μ-unitr ; μ-assoc ; module unit ; module mult) public
+
+ ℝ : Monad-on R
+ ℝ = record { has-is-monad = R-monad }
+```
+
+:::{.definition #algebraic-weak-factorisation-system alias="awfs"}
+An **algebraic weak factorisation system** on $\cC$ is a [[functorial
+factorisation]] $F$ which is simultaneously equipped with [[left|left
+weak factorisation structure]] and [[right weak factorisation
+structures]].
+:::
+
+```agda
+ record Awfs-on : Type (o ⊔ ℓ) where
+ field
+ awfsᴸ : Lwfs-on
+ awfsᴿ : Rwfs-on
+
+ open Lwfs-on awfsᴸ public
+ open Rwfs-on awfsᴿ public
+```
+
+The most important consequence of $L$ being a comonad and $R$ being a
+monad is that any map with an $L$-coalgebra structure lifts against maps
+with $R$-algebras.
+
+```agda
+ L-R-lifts
+ : ∀ {a b x y} {f : Hom a b} {g : Hom x y}
+ → Coalgebra-on 𝕃 (_ , _ , f)
+ → Algebra-on ℝ (_ , _ , g)
+ → ∀ {u v} → v ∘ f ≡ g ∘ u → Lifting C f g u v
+ L-R-lifts {f = f} {g = g} Lf Rg {u} {v} vf=gu = record where
+ module f = Coalgebra-on Lf
+ module g = Algebra-on Rg
+ open Interpolant (F .S₁ record{ com = sym vf=gu })
+ renaming (map to h ; sq₀ to α ; sq₁ to β)
+
+ rem₁ : g ∘ g.ν .top ≡ ρ→ g
+ rem₁ = g.ν .com ∙ eliml (intror refl ∙ ap bot g.ν-unit)
+
+ rem₂ : f.ρ .bot ∘ f ≡ λ→ f
+ rem₂ = sym (intror (introl refl ∙ ap top f.ρ-counit) ∙ f.ρ .com)
+
+ fst = g.ν .top ∘ h ∘ f.ρ .bot
+ snd = pullr (pullr rem₂) ∙ pushr (sym α) ∙ eliml (ap top g.ν-unit)
+ , pulll rem₁ ∙ extendl β ∙ elimr (ap bot f.ρ-counit)
+```
+
+
+
+## Lifts in a lwfs
+
+```agda
+ whisker-ρ : ∀ {u v w x} {f : Hom u v} {g : Hom w x} → Homᵃ C f g → Homᵃ C f (ρ→ g)
+ whisker-ρ sq .top = λ→ _ ∘ sq .top
+ whisker-ρ sq .bot = sq .bot
+ whisker-ρ sq .com = pulll (sym (factors _)) ∙ sq .com
+
+ lift-λρ
+ : ∀ {u v w x} {f : Hom u v} {g : Hom w x} (σ : Homᵃ C (λ→ f) g)
+ → Square-lift (whisker-ρ σ)
+ lift-λρ {f = f} {g} σ = record { snd = α , β } where abstract
+ α : (Ff.map σ ∘ δ f) ∘ λ→ f ≡ λ→ g ∘ σ .top
+ α = pullr (sym (δˢ f .com) ∙ elimr δ-top) ∙ sym (F .S₁ σ .sq₀)
+
+ β : ρ→ g ∘ Ff.map σ ∘ δ f ≡ σ .bot
+ β = pulll (F .S₁ σ .sq₁) ∙ cancelr δ-unitr
+```
diff --git a/src/Cat/Morphism/Lifts.lagda.md b/src/Cat/Morphism/Lifts.lagda.md
index 08e55588b..7070d9d4d 100644
--- a/src/Cat/Morphism/Lifts.lagda.md
+++ b/src/Cat/Morphism/Lifts.lagda.md
@@ -57,6 +57,13 @@ that $w \circ f = u$ and $g \circ w = v$.
Lifting {a} {b} {x} {y} f g u v = Σ[ w ∈ Hom b x ] w ∘ f ≡ u × g ∘ w ≡ v
```
+
+
:::{.definition #lifts-against}
Let $f, g$ be two morphisms of $\cC$. We say that $f$ *left lifts against* $g$
and $g$ *right lifts against* $f$ if for every commutative square
diff --git a/src/preamble.tex b/src/preamble.tex
index bbfb75f60..79d55c84e 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -51,10 +51,13 @@
\newcommand{\ica}[1]{\mathbb{#1}} % Names of internal categories
\newcommand{\Arr}[1]{%% The arrow category of a category.
- \rm{Arr}(#1)
+ \operatorname{\thecat{Arr}}(#1)
}
\newcommand{\FAlg}[1]{%% The category of F-algebras
- \rm{Alg}(#1)
+ \operatorname{\thecat{Alg}}(#1)
+}
+\newcommand{\Ff}[1]{%% The category of functorial factorisations
+ \operatorname{\thecat{Ff}}(#1)
}
% \liesover arrow is only allowed in KaTeX: