Functorial factorisation systems and co.

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))

src/Cat/Diagram/Comonad.lagda.md

@@ -28,36 +28,50 @@ 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
 ```
 
 <!--
 ```agda
+    no-eta-equality
+    open Functor W renaming (F₀ to W₀ ; F₁ to W₁ ; F-id to W-id ; F-∘ to W-∘) public
+
     module counit = _=>_ counit renaming (η to ε)
     module comult = _=>_ comult renaming (η to δ)
 
-    open Functor W renaming (F₀ to W₀ ; F₁ to W₁ ; F-id to W-id ; F-∘ to W-∘) public
     open counit using (ε) public
     open comult using (δ) public
 ```
 -->
 
-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
       δ-unitr : ∀ {x} → ε (W₀ x) ∘ δ x ≡ id
       δ-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
+```
+
+<!--
+```agda
+    open is-comonad has-is-comonad public
+
+unquoteDecl H-Level-is-comonad = declare-record-hlevel 1 H-Level-is-comonad (quote is-comonad)
+```
+-->
+
 <!--
 ```agda
 module _ {o h : _} {C : Precategory o h} {F G : Functor C C} {M : Comonad-on F} {N : Comonad-on G} where

src/Cat/Diagram/Comonad/Writer.lagda.md

@@ -12,6 +12,8 @@ open import Cat.Prelude
 import Cat.Reasoning as Cat
 
 open Comonad-on
+open is-comonad
+open is-monad
 open Monad-on
 open Functor
 open _=>_
@@ -76,11 +78,11 @@ them in this `<details>`{.html} block for the curious reader.</summary>
   Writer-comonad .comult .is-natural x y f = unique₂
     (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ idl _)
     (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ cancelr π₂∘⟨⟩)
-  Writer-comonad .δ-unitl = unique₂
+  Writer-comonad .has-is-comonad .δ-unitl = unique₂
     (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ cancelr π₂∘⟨⟩)
     (idr _) (idr _)
-  Writer-comonad .δ-unitr = π₂∘⟨⟩
-  Writer-comonad .δ-assoc = ⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ refl (pullr π₂∘⟨⟩ ∙ id-comm) ∙ sym (⟨⟩∘ _)
+  Writer-comonad .has-is-comonad .δ-unitr = π₂∘⟨⟩
+  Writer-comonad .has-is-comonad .δ-assoc = ⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ refl (pullr π₂∘⟨⟩ ∙ id-comm) ∙ sym (⟨⟩∘ _)
 ```
 
 </details>
@@ -129,23 +131,23 @@ products.
       (pulll π₁∘⟨⟩ ∙ π₁∘⟨⟩ ∙ sym (pullr (sym (!-unique _))))
       (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idr f)
     mk .mult .is-natural x y f = products! products
-    mk .μ-unitr =
+    mk .has-is-monad .μ-unitr =
       let
         lemma =
           m.μ ∘ ⟨ π₁ , m.η ∘ ! ∘ π₂ ⟩               ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ idl π₁) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ ap₂ _∘_ refl (!-unique _))) ⟩
           m.μ ∘ ⟨ id ∘ π₁ , m.η ∘ π₂ ⟩ ∘ ⟨ π₁ , ! ⟩ ≡⟨ pulll m.μ-unitr ⟩
           π₁ ∘ ⟨ π₁ , ! ⟩                           ≡⟨ π₁∘⟨⟩ ⟩
           π₁                                        ∎
       in ⟨⟩-unique₂ (products! products ∙ lemma) (products! products) (idr π₁) (idr π₂)
-    mk .μ-unitl =
+    mk .has-is-monad .μ-unitl =
       let
         lemma =
           m.μ ∘ ⟨ m.η ∘ ! , π₁ ⟩                    ≡˘⟨ ap₂ _∘_ refl (⟨⟩-unique (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl π₁)) ⟩
           m.μ ∘ ⟨ m.η ∘ π₁ , id ∘ π₂ ⟩ ∘ ⟨ ! , π₁ ⟩ ≡⟨ pulll m.μ-unitl ⟩
           π₂ ∘ ⟨ ! , π₁ ⟩                           ≡⟨ π₂∘⟨⟩ ⟩
           π₁                                        ∎
       in ⟨⟩-unique₂ (products! products ∙ lemma) (products! products) (idr π₁) (idr π₂)
-    mk .μ-assoc {x} =
+    mk .has-is-monad .μ-assoc {x} =
       let
         lemma =
           π₁ ∘ ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ∘ ⟨ π₁ , ⟨ m.μ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩ ∘ π₂ ⟩

src/Cat/Diagram/Monad.lagda.md

@@ -45,16 +45,11 @@ M$.
 More generally, we define what it means to equip a *fixed* functor $M$
 with the structure of a monad. The notion of "monad on a category" is
 obtained by pairing the functor $M$ with the monad structure $\eta,
-\mu$.
-
-[monoid]: Algebra.Monoid.html
+\mu$.  More generally, we can fix the functor *and* the maps, and define
+the laws that make that entire triple into a monad.
 
 ```agda
-  record Monad-on (M : Functor C C) : Type (o ⊔ h) where
-    no-eta-equality
-    field
-      unit : Id => M
-      mult : M F∘ M => M
+  record is-monad {M : Functor C C} (unit : Id => M) (mult : M F∘ M => M) : Type (o ⊔ h) where
 ```
 
 <!--
@@ -68,16 +63,25 @@ obtained by pairing the functor $M$ with the monad structure $\eta,
 ```
 -->
 
-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
       μ-unitl : ∀ {x} → μ x C.∘ η (M₀ x) ≡ C.id
       μ-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}

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.</summary>
 
 ```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.</summary>
           ∙ 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.</summary>
           ∙∙ 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 _ _ _)

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-∘ _ _ ⟩

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