open import Cat.Diagram.Monad.Relative
open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Reasoning

open Functor
open _=>_

module Cat.Diagram.Monad.Extension where

module _ {o ℓ} (C : Precategory o ℓ) where

Extension systems🔗

An extension system on a category $\mathcal{C}$ is an alternative way of presenting a monad on $\mathcal{C}\text{.}$ As the name suggests, extension systems are built around an extension operation, of type $\mathcal{C}(X,MY)\to \mathcal{C}(MX,MY)\text{,}$ in place of the multiplication operation $\mathcal{C}(MMX,MX)$ that characterises a monad. This has a couple of immediate benefits:

1. The extension operation avoids nested applications of $M\text{,}$ which tends to improve ergonomics.

2. The extension operation $\mathcal{C}(X,MY)\to \mathcal{C}(MX,MY)$ simultaneously encodes both $M\text{’s}$ multiplication and its underlying functorial action, which reduces the amount of data that needs to be given explicitly.

3. It is not immediately clear how to generalize monads beyond endofunctors. In constrast, extension systems can be readily generalized to relative extension systems¹.

With that bit of motivation out of the way, we shall proceed to define extension systems. An extension system consists of:

1. A mapping of objects, $M:\mathcal{C}\to \mathcal{C}\text{;}$ and

2. A family of morphisms ${\eta }_X:\mathcal{C}(X,MX)\text{,}$ called the unit of the extension system; and

3. The extension operation, $(-{)}^M:\mathcal{C}(X,MY)\to \mathcal{C}(MX,MY)\text{.}$ Gesturing towards the “monads” found in functional programming, we will call this operation bind.

Note that we do not require the mapping of objects to be functorial, nor the do we require the unit to be natural. Instead, we impose 3 equations on this structure:²

1. For every $X:\mathcal{C}\text{,}$ we must have $({\eta }_X{)}^M={\mathrm{id}}_{MX}\text{;}$
2. For every $f:\mathcal{C}(X,MY)\text{,}$ we must have $f^M\circ {\eta }_X=f\text{;}$ and
3. For every $f:\mathcal{C}(Y,MX)\text{,}$ and $g:\mathcal{C}(X,MY)\text{,}$ we must have $f^M\circ g^M=(f^M\circ g{)}^M\text{.}$

For reasons of generality, we shall define extension systems as relative extension systems, along the identity functor. Even though we use a more general definition, the data contained in an extension system is precisely the data listed above.

Extension-system : ∀ {o ℓ} → Precategory o ℓ → Type (o ⊔ ℓ)
Extension-system C = Relative-extension-system (Id {C = C})

module Extension-system {o ℓ} {C : Precategory o ℓ} (E : Extension-system C) where
  open Cat.Reasoning C
  open Relative-extension-system E public

We can recover the monad’s multiplication by extending the identity morphism ${\mathrm{id}}_{MX}:\mathcal{C}(MX,MX)\text{.}$

  join : ∀ {x} → Hom (M₀ (M₀ x)) (M₀ x)
  join {x} = bind (id {M₀ x})

Naturality of join also follows, though is a bit more involved.

  join-natural
    : ∀ {x y} (f : Hom x y)
    → join ∘ M₁ (M₁ f) ≡ M₁ f ∘ join
  join-natural f =
    bind id ∘ bind (unit ∘ bind (unit ∘ f)) ≡⟨ bind-∘ id (unit ∘ bind (unit ∘ f)) ⟩≡
    bind (bind id ∘ unit ∘ bind (unit ∘ f)) ≡⟨ ap bind (cancell (bind-unit-∘ id) ∙ sym (idr _)) ⟩≡
    bind (bind (unit ∘ f) ∘ id)             ≡˘⟨ bind-∘ (unit ∘ f) id ⟩≡˘
    bind (unit ∘ f) ∘ bind id               ∎

Equivalence with monads🔗

module _ {o ℓ} {C : Precategory o ℓ} where
  open Cat.Reasoning C

It remains to show that monads on $\mathcal{C}$ are equivalent to extension systems on $\mathcal{C}\text{.}$ We’ll start with the forward direction. Throughout, let $M$ be a fixed monad on $\mathcal{C}\text{.}$

  Monad→Extension-system : Monad C → Extension-system C
  Monad→Extension-system M = system where
    module M = Monad M
    open Extension-system

The mapping of objects, and the unit, are directly given by (the object part of) $M\text{-qua-endofunctor,}$ and by the unit natural transformation.

    system : Extension-system C
    system .M₀ = M.M₀
    system .unit = M.η _

Defining the extension operation is slightly trickier, but not by much. If we have a morphism $f:\mathcal{C}(X,MY)\text{,}$ then its extension is defined to be composite

    system .bind f = M.μ _ ∘ M.M₁ f

Finally, a few short computations show that this definition is lawful.

    system .bind-unit-id =
      M.μ _ ∘ M.M₁ (M.η _) ≡⟨ M.left-ident ⟩≡
      id                             ∎
    system .bind-unit-∘ f =
      (M.μ _ ∘ M.M₁ f) ∘ M.η _ ≡⟨ pullr (sym $ M.unit.is-natural _ _ _) ⟩≡
      M.μ _ ∘ M.η _ ∘ f        ≡⟨ cancell M.right-ident ⟩≡
      f                        ∎
    system .bind-∘ f g =
      (M.μ _ ∘ M.M₁ f) ∘ (M.μ _ ∘ M.M₁ g)             ≡⟨ pullr (extendl (sym $ M.mult.is-natural _ _ _)) ⟩≡
      M.μ _ ∘ M.μ _ ∘ (M.M₁ (M.M₁ f) ∘ M.M₁ g)        ≡⟨ extendl (sym M.mult-assoc) ⟩≡
      M.μ _ ∘ M.M₁ (M.μ _) ∘ (M.M₁ (M.M₁ f) ∘ M.M₁ g) ≡⟨ ap₂ _∘_ refl (pulll (sym (M.M-∘ _ _)) ∙ sym (M.M-∘ _ _)) ⟩≡
      M.μ _ ∘ M.M₁ ((M.μ _ ∘ M.M₁ f) ∘ g)             ∎

Constructing a monad from an extension system is simply a matter of bolting together our results from the previous section.

  Extension-system→Monad : Extension-system C → Monad C
  Extension-system→Monad E = monad where
    module E = Extension-system E
    open Monad

    monad : Monad C
    monad .M = E.M
    monad .unit .η x = E.unit
    monad .unit .is-natural _ _ f = E.unit-natural f
    monad .mult .η x = E.join
    monad .mult .is-natural _ _ f = E.join-natural f

The monad laws follow from another short series of computations.

    monad .left-ident =
      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 .right-ident =
      E.bind id ∘ E.unit ≡⟨ E.bind-unit-∘ id ⟩≡
      id                 ∎
    monad .mult-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-∘ _ _ ⟩≡˘
      E.bind id ∘ E.bind id                   ∎

Moreover, these two functions constitute an equivalence between monads on $\mathcal{C}$ and extension systems on $\mathcal{C}\text{.}$ In light of this fact, we will silently identify monads and extension systems, whenever it is convenient.

  Monad≃Extension-system : Monad C ≃ Extension-system C
  Monad≃Extension-system = Iso→Equiv $
    Monad→Extension-system ,
    iso Extension-system→Monad
      (λ E →
        let module E = Extension-system E in
        Relative-extension-system-path
          (λ _ → refl)
          (λ _ → refl)
          (λ f →
            E.bind id ∘ E.bind (E.unit ∘ f i0) ≡⟨ E.bind-∘ id (E.unit ∘ f i0) ⟩≡
            E.bind (E.bind id ∘ E.unit ∘ f i0) ≡⟨ ap E.bind (cancell (E.bind-unit-∘ id)) ⟩≡
            E.bind (f i0)                      ≡⟨ ap E.bind (coe0→1 (λ i → f i0 ≡ f i) refl) ⟩≡
            E.bind (f i1)                      ∎))
      (λ M →
        let module M = Monad M in
        Monad-path
          (λ _ → refl)
          (λ f →
            M.μ _ ∘ M.M₁ (M.η _ ∘ f)        ≡⟨ pushr (M.M-∘ _ _) ⟩≡
            (M.μ _ ∘ M.M₁ (M.η _)) ∘ M.M₁ f ≡⟨ eliml M.left-ident ⟩≡
            M.M₁ f ∎)
          (λ _ → refl)
          (λ _ → elimr M.M-id))

Algebras over an extension system🔗

An extension algebra over $E$ is the extension system analog of a algebra over a monad. Following the general theme of extension operations, an extension algebra on $X:\mathcal{C}$ is given by an operation $\nu :\mathcal{C}(A,X)\to \mathcal{C}(MA,X)\text{.}$ Intuitively, this operation lets us “evaluate” any $M\text{,}$ so long as the codomain of the evaluation is $X\text{.}$

This operation must satisfy a pair of equations:

1. For every $f:\mathcal{C}(A,X)\text{,}$ we have $\nu (f)\circ {\eta }_A=f\text{;}$ and
2. For every $f:\mathcal{C}(B,X)\text{,}$ and $g:\mathcal{C}(A,MB)\text{,}$ we have $\nu (f)\circ g^M=\nu (\nu f\circ g)\text{.}$

As with extension systems, we define extension algebras in terms of relative extension algebras.

Extension-algebra-on
  : ∀ {o ℓ} {C : Precategory o ℓ}
  → (open Precategory C)
  → Extension-system C
  → Ob
  → Type (o ⊔ ℓ)
Extension-algebra-on = Relative-algebra-on

module Extension-algebra-on
  {o ℓ} {C : Precategory o ℓ} (open Cat.Reasoning C)
  {E : Extension-system C} {x : Ob} (α : Extension-algebra-on E x)
  where
  open Extension-system E
  open Relative-algebra-on α public

The evaluation map also interacts well with the multiplication.

  ν-join : ∀ {a} (f : Hom a x) → ν f ∘ join ≡ ν (ν f)
  ν-join f =
    ν f ∘ bind id ≡⟨ ν-bind f id ⟩≡
    ν (ν f ∘ id)  ≡⟨ ap ν (idr _) ⟩≡
    ν (ν f)       ∎

Equivalence with monad algebras🔗

module _ {o ℓ} {C : Precategory o ℓ} {E : Extension-system C} where
  open Cat.Reasoning C
  open Extension-system E
  open Extension-algebra-on

As the name suggests, extension algebras over $E$ are equivalent to monad algebras over the canonical monad associated with $E\text{.}$

For the forward direction, let $\alpha :MX\to X$ be a monad algebra over $E\text{.}$ We can obtain the required extension operation $\nu$ by sending each $f:\mathcal{C}(A,X)$ to the composite

  Algebra-on→Extension-algebra-on
    : ∀ {x}
    → Algebra-on C (Extension-system→Monad E) x
    → Extension-algebra-on E x
  Algebra-on→Extension-algebra-on {x = x} α = ext-alg where
    module α = Algebra-on α
    open Extension-algebra-on

    ext-alg : Extension-algebra-on E x
    ext-alg .ν f = α.ν ∘ M₁ f

    ext-alg .ν-unit f =
      (α.ν ∘ M₁ f) ∘ unit ≡⟨ pullr (sym $ unit-natural f) ⟩≡
      α.ν ∘ unit ∘ f      ≡⟨ cancell α.ν-unit ⟩≡
      f ∎
    ext-alg .ν-bind f g =
      (α.ν ∘ M₁ f) ∘ bind g                    ≡⟨ pullr (bind-naturall _ _) ⟩≡
      α.ν ∘ bind ⌜ M₁ f ∘ g ⌝                  ≡⟨ ap! (insertl (bind-unit-∘ id)) ⟩≡
      α.ν ∘ bind (join ∘ unit ∘ M₁ f ∘ g)      ≡⟨ pushr (sym (bind-∘ _ _)) ⟩≡
      (α.ν ∘ join) ∘ bind (unit ∘ M₁ f ∘ g)    ≡⟨ pushl (sym $ α.ν-mult) ⟩≡
      α.ν ∘ M₁ α.ν ∘ bind (unit ∘ M₁ f ∘ g)    ≡⟨ ap (α.ν ∘_) (bind-naturall _ _) ⟩≡
      α.ν ∘ bind ⌜ M₁ α.ν ∘ unit ∘ M₁ f ∘ g ⌝  ≡⟨ ap! (centralizel (sym $ unit-natural _)) ⟩≡
      α.ν ∘ bind (unit ∘ (α.ν ∘ M₁ f) ∘ g)     ∎

Conversely, a monad algebra over $E$ can be derived from an extension algebra $\nu :\mathcal{C}(A,X)\to \mathcal{C}(MA,X)$ over $E$ by restricting to $\nu ({\mathrm{id}}_X):\mathcal{C}(MX,X)\text{.}$

  Extension-algebra-on→Algebra-on
    : ∀ {x}
    → Extension-algebra-on E x
    → Algebra-on C (Extension-system→Monad E) x
  Extension-algebra-on→Algebra-on {x = x} α = alg where
    module α = Extension-algebra-on α
    open Algebra-on

    alg : Algebra-on C (Extension-system→Monad E) x
    alg .ν = α.ν id

The proofs of the monad algebra laws are mercifully short.

    alg .ν-unit = α.ν-unit id
    alg .ν-mult =
      α.ν id ∘ M₁ (α.ν id) ≡⟨ α.ν-natural _ _ ⟩≡
      α.ν (id ∘ α.ν id)    ≡⟨ ap α.ν (idl _) ⟩≡
      α.ν (α.ν id)         ≡˘⟨ α.ν-join id ⟩≡˘
      α.ν id ∘ join ∎

As expected, these two functions constitute an equivalence between monad algebras and extension algebras.

  Algebra-on≃Extension-algebra-on
    : ∀ {x}
    → Algebra-on C (Extension-system→Monad E) x ≃ Extension-algebra-on E x
  Algebra-on≃Extension-algebra-on {x} = Iso→Equiv $
    Algebra-on→Extension-algebra-on ,
    iso Extension-algebra-on→Algebra-on
      (λ α →
        let module α = Extension-algebra-on α in
        Relative-algebra-on-pathp refl λ f →
          α.ν id ∘ M₁ (f i0) ≡⟨ α.ν-natural _ _ ⟩≡
          α.ν (id ∘ f i0)    ≡⟨ ap α.ν (idl _) ⟩≡
          α.ν (f i0)         ≡⟨ ap α.ν (coe0→1 (λ i → f i0 ≡ f i) refl) ⟩≡
          α.ν (f i1)         ∎)
      (λ α →
        let module α = Algebra-on α in
        Algebra-on-pathp C refl $
          α.ν ∘ bind (unit ∘ id) ≡⟨ elimr (ap bind (idr _) ∙ bind-unit-id) ⟩≡
          α.ν                    ∎)