module Cat.Diagram.Monad.Extension where

Extension systems🔗

An extension system on a category is an alternative way of presenting a monad on As the name suggests, extension systems are built around an extension operation, of type in place of the multiplication operation that characterises a monad. This has a couple of immediate benefits:

  1. The extension operation avoids nested applications of which tends to improve ergonomics.

  2. The extension operation simultaneously encodes both 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 systems1.

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, and

  2. A family of morphisms called the unit of the extension system; and

  3. The extension operation, 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:2

  1. For every we must have
  2. For every we must have and
  3. For every and we must have

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

  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🔗

It remains to show that monads on are equivalent to extension systems on We’ll start with the forward direction. Throughout, let be a fixed monad on

  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) 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 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 and extension systems on 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 is the extension system analog of a algebra over a monad. Following the general theme of extension operations, an extension algebra on is given by an operation Intuitively, this operation lets us “evaluate” any so long as the codomain of the evaluation is

This operation must satisfy a pair of equations:

  1. For every we have and
  2. For every and we have

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🔗

As the name suggests, extension algebras over are equivalent to monad algebras over the canonical monad associated with

For the forward direction, let be a monad algebra over We can obtain the required extension operation by sending each 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
The monad algebra laws follow from some tedious calculations that we shall omit.
    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 can be derived from an extension algebra over by restricting to

  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) ⟩≡
          α.Îœ                    ∎)

  1. In fact, we will define extension systems as a special case of relative extension systems!↩

  2. contrast this with the 7 equations required for a monad: 2 for functoriality, 2 for naturality, and 3 for unitality/associativity↩