open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Monad.Relative
open import Cat.Functor.Adjoint.Monad
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Equivalence
open import Cat.Diagram.Initial
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Displayed.Base
open import Cat.Diagram.Monad
open import Cat.Prelude

open import Data.Nat

open import Order.Instances.Nat
open import Order.Cat

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Functor.Algebra where

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

Algebras over an endofunctor🔗

  private module F = Cat.Functor.Reasoning F
  open Cat.Reasoning C
  open Displayed
  open Total-hom

Let $F:\mathcal{C}\to \mathcal{C}$ be an arbitrary endofunctor on $\mathcal{C}\text{.}$ We can view $F$ as a means of embellishing an object with extra structure: for instance, the functor $X\mapsto X+1$ endows $X$ with an additional point and an endomap $X\to X\text{,}$ the functor $X\mapsto A\times X+1$ adds an extra point and a copy of $A\text{,}$ etc. Consequently, a map $\mathcal{C}(F(A),A)$ picks out a suitably structured $A\text{;}$ e.g. writing a map $\mathcal{C}(A+1,A)$ requires $A$ to be equipped with a global element and an endomap $\mathcal{C}(A,A)\text{.}$ In analogy to monad algebras, a map $\mathcal{C}(F(A),A)$ is called an F-algebra on $A$¹.

Likewise, a map $f:\mathcal{C}(A,B)$ between two $F\text{-algebras}$ $\alpha :\mathcal{C}(F(A),A)$ and $\beta :\mathcal{C}(F(B),B)$ is an F-algebra homomorphism if it commutes with the algebras on $A$ and $B\text{,}$ as in the following digram.

Intuitively, $F\text{-algebra}$ morphisms are morphisms that preserve the structure encoded by $F\text{;}$ going back to our previous example, an $F\text{-algebra}$ homomorphism between $\alpha :A+1\to A$ and $\beta :B+1\to B$ is a map $f:A\to B$ that preserves the designated global elements of $A$ and $B$ and commutes with the chosen endomaps.

We can assemble $F\text{-algebras}$ into a displayed category over $\mathcal{C}\text{:}$ the type of objects over $A$ consists of all possible algebra structures on $A\text{,}$ and the type of morphisms over $f:\mathcal{C}(A,B)$ are proofs that $f$ is an $F\text{-algebra}$ homomorphism.

  F-Algebras : Displayed C ℓ ℓ
  F-Algebras .Ob[_] a = Hom (F.₀ a) a
  F-Algebras .Hom[_] f α β = f ∘ α ≡ β ∘ F.₁ f
  F-Algebras .Hom[_]-set _ _ _ = hlevel 
  F-Algebras .id' = idl _ ∙ intror F.F-id
  F-Algebras ._∘'_ p q = pullr q ∙ pulll p ∙ pullr (sym (F.F-∘ _ _))
  F-Algebras .idr' _ = prop!
  F-Algebras .idl' _ = prop!
  F-Algebras .assoc' _ _ _ = prop!

We can take the total category of this displayed category to recover the more traditional category of $F\text{-algebras.}$

  FAlg : Precategory (o ⊔ ℓ) ℓ
  FAlg = ∫ F-Algebras

  module FAlg = Cat.Reasoning FAlg

  F-Algebra : Type _
  F-Algebra = FAlg.Ob

Lambek’s lemma🔗

As noted above, $F\text{-algebras}$ are a tool for picking out objects equipped with a semantics for a “signature” described by $F\text{.}$ This leads to a very natural question: can we characterize the syntax generated from the signature of $F\text{?}$

To answer this question, we must pin down exactly what we mean by “syntax”. Categorically, we have two options: initial objects, and free objects; these correspond to “syntax” and “syntax with generators”, respectively. We will focus initial $F\text{-algebras}$ for now: free objects are much harder to come by, and initial $F\text{-algebras}$ have a nice characterization: they are the least fixpoints of functors. This result is known as Lambek’s lemma, and we shall prove it now.

First, a tiny lemma. Let $(A,\alpha )$ be an $F\text{-algebra,}$ and note that $(F(A),F(\alpha ))$ is also an $F\text{-algebra.}$ If $\alpha$ has a section $f:(A,\alpha )\to (F(A),F(\alpha ))\text{,}$ then $f$ and $\alpha$ are inverses.

  algebra-section→inverses
    : ∀ {a} (α : Hom (F.₀ a) a)
    → (f : FAlg.Hom (a , α) (F.₀ a , F.₁ α))
    → f .hom section-of α
    → Inverses α (f .hom)
  algebra-section→inverses α f section =
    make-inverses section $
      f .hom ∘ α           ≡⟨ f .preserves ⟩≡
      F.₁ α ∘ F.₁ (f .hom) ≡⟨ F.annihilate section ⟩≡
      id                   ∎

On to the main result. Let $(A,\alpha )$ be an initial $F\text{-algebra.}$ As before, $(F(A),F(\alpha ))$ is also an $F\text{-algebra,}$ so initiality gives us a unique $F\text{-algebra}$ morphism $\text{unroll}:(A,\alpha )\to (F(A),F(\alpha ))\text{.}$ Likewise, $\alpha$ induces an $F\text{-algebra}$ morphism $\text{roll}:(F(A),F(\alpha )\to (A,\alpha ))\text{.}$ Furthermore, $\text{unroll}$ is a section of $\text{roll}\text{,}$ as maps out of the initial object are unique. Therefore, $\text{unroll}$ must also be an inverse, so $\alpha$ is invertible.

  lambek : ∀ {a} (α : Hom (F.₀ a) a) → is-initial FAlg (a , α) → is-invertible α
  lambek {a} α initial = inverses→invertible $
    algebra-section→inverses α unroll roll-unroll
    where
      unroll : FAlg.Hom (a , α) (F.₀ a , F.₁ α)
      unroll = initial (F.₀ a , F.₁ α) .centre

      roll : FAlg.Hom (F.₀ a , F.₁ α) (a , α)
      roll .hom = α
      roll .preserves = refl

      roll-unroll : α ∘ unroll .hom ≡ id
      roll-unroll =
        ap hom $
        is-contr→is-prop (initial (a , α)) (roll FAlg.∘ unroll) FAlg.id

This result means that an initial $F\text{-algebra}$ $(A,\alpha )$ is a fixpoint of the functor $F\text{,}$ and should be thought of as the the object $F(F(F(\cdots )))\text{.}$ The canonical example is the initial algebra of $X\mapsto 1+X\text{:}$ if it exists, this will be an object of the form $1+(1+(1+\cdots ))\text{:}$ in $\mathbf{Sets}\text{,}$ this initial algebra is the natural numbers! In general, initial $F\text{-algebras}$ are how we give a categorical semantics to non-indexed inductive datatypes like Nat or List.

Adámek’s fixpoint theorem🔗

Note that initial $F\text{-algebras}$ need not exist for a given functor $F\text{.}$ Nevertheless, Adámek’s fixpoint theorem lets us construct some initial $F\text{-algebras,}$ provided that:

1. $\mathcal{C}$ has an initial object.
2. $\mathcal{C}$ has a colimit for the diagram:

3. $F$ preserves the aforementioned colimit.

Note that this construction is precisely a categorified version of Kleene’s fixpoint theorem, so we will be following the exact same proof strategy.

We begin by constructing the above diagram as a functor $F^{(-)}(\perp ):\omega \to \mathcal{C}\text{,}$ where $\omega$ is the poset of natural numbers, regarded as a category.

  private
    ω : Precategory _ _
    ω = poset→category Nat-poset

  module _
    (initial : Initial C)
    where

    open Functor
    open Initial initial

    F₀ⁿ[⊥] : Nat → Ob
    F₀ⁿ[⊥] zero = bot
    F₀ⁿ[⊥] (suc n) = F.₀ (F₀ⁿ[⊥] n)

    F₁ⁿ[⊥] : ∀ {m n} → m ≤ n → Hom (F₀ⁿ[⊥] m) (F₀ⁿ[⊥] n)
    F₁ⁿ[⊥] 0≤x = ¡
    F₁ⁿ[⊥] (s≤s p) = F.₁ (F₁ⁿ[⊥] p)

    Fⁿ[⊥] : Functor ω C

    Fⁿ[⊥]-id : ∀ n → F₁ⁿ[⊥] (≤-refl {n}) ≡ id
    Fⁿ[⊥]-id zero = ¡-unique id
    Fⁿ[⊥]-id (suc n) = F.elim (Fⁿ[⊥]-id n)

    Fⁿ[⊥]-∘
      : ∀ {m n o}
      → (p : n ≤ o) (q : m ≤ n)
      → F₁ⁿ[⊥] (≤-trans q p) ≡ F₁ⁿ[⊥] p ∘ F₁ⁿ[⊥] q
    Fⁿ[⊥]-∘ p 0≤x = ¡-unique₂ _ _
    Fⁿ[⊥]-∘ (s≤s p) (s≤s q) = F.expand (Fⁿ[⊥]-∘ p q)

    Fⁿ[⊥] .F₀ = F₀ⁿ[⊥]
    Fⁿ[⊥] .F₁ = F₁ⁿ[⊥]
    Fⁿ[⊥] .F-id {n} = Fⁿ[⊥]-id n
    Fⁿ[⊥] .F-∘ p q = Fⁿ[⊥]-∘ p q

Next, note that every $F\text{-algebra}$ $(A,\alpha )$ can be extended to a morphism $\mathcal{C}(F^n(\perp ),A)\text{.}$ Furthermore, this extension is natural in $n\text{.}$

    Fⁿ[⊥]-fold : ∀ {a} → Hom (F.₀ a) a → ∀ n → Hom (F₀ⁿ[⊥] n) a
    Fⁿ[⊥]-fold α zero = ¡
    Fⁿ[⊥]-fold α (suc n) = α ∘ F.₁ (Fⁿ[⊥]-fold α n)

    Fⁿ[⊥]-fold-nat
      : ∀ {a} {α : Hom (F.₀ a) a} {m n}
      → (m≤n : m ≤ n)
      → Fⁿ[⊥]-fold α n ∘ F₁ⁿ[⊥] m≤n ≡ Fⁿ[⊥]-fold α m
    Fⁿ[⊥]-fold-nat 0≤x = sym (¡-unique _)
    Fⁿ[⊥]-fold-nat (s≤s m≤n) = F.pullr (Fⁿ[⊥]-fold-nat m≤n)

Now, suppose that $\mathcal{C}$ has a colimit $F^{\infty }(\perp )$ of the diagram $F^{(-)}(\perp )\text{,}$ and $F$ preserves this colimit. We can equip $F^{\infty }(\perp )$ with an $F\text{-algebra}$ $\mathrm{roll}:F(F^{\infty }(\perp ))\to F^{\infty }(\perp )$ by using the universal property of the colimit $F(F^{\infty }(\perp ))\text{.}$

    adamek : Colimit Fⁿ[⊥] → preserves-colimit F Fⁿ[⊥] → Initial FAlg
    adamek Fⁿ[⊥]-colim F-pres-Fⁿ[⊥]-colim = ∐Fⁿ[⊥]-initial
      module adamek where
      module ∐Fⁿ[⊥] = Colimit Fⁿ[⊥]-colim
      module F[∐Fⁿ[⊥]] = is-colimit (F-pres-Fⁿ[⊥]-colim ∐Fⁿ[⊥].has-colimit)

      ∐Fⁿ[⊥] : Ob
      ∐Fⁿ[⊥] = ∐Fⁿ[⊥].coapex

      roll : Hom (F.₀ ∐Fⁿ[⊥]) ∐Fⁿ[⊥]
      roll = F[∐Fⁿ[⊥]].universal (∐Fⁿ[⊥].ψ ⊙ suc) (∐Fⁿ[⊥].commutes ⊙ s≤s)

Next, we can extend any F-algebra $(A,\alpha )$ to a morphism $F^{\infty }(\perp )$ by using the universal property, along with the extensions $\mathcal{C}(F^n(\perp ),A)$ we constructed earlier.

      fold : ∀ {a} → Hom (F.₀ a) a → Hom ∐Fⁿ[⊥] a
      fold α = ∐Fⁿ[⊥].universal (Fⁿ[⊥]-fold α) Fⁿ[⊥]-fold-nat

This extension commutes with $\mathrm{roll}\text{,}$ and thus induces an $F\text{-algebra}$ morphism $(F^{\infty }(\perp ),\mathrm{roll})\to (A,\alpha )\text{.}$

      fold-roll : ∀ {a} (α : Hom (F.₀ a) a) → fold α ∘ roll ≡ α ∘ F.₁ (fold α)
      fold-roll α =
        F[∐Fⁿ[⊥]].unique₂ (Fⁿ[⊥]-fold α ⊙ suc) (Fⁿ[⊥]-fold-nat ⊙ s≤s)
          (λ j →
            (fold α ∘ roll) ∘ F.₁ (∐Fⁿ[⊥].ψ j) ≡⟨ pullr (F[∐Fⁿ[⊥]].factors _ _) ⟩≡
            fold α ∘ ∐Fⁿ[⊥].ψ (suc j)          ≡⟨ ∐Fⁿ[⊥].factors _ _ ⟩≡
            Fⁿ[⊥]-fold α (suc j)               ∎)
          (λ j →
            (α ∘ F.₁ (fold α)) ∘ F.₁ (∐Fⁿ[⊥].ψ j) ≡⟨ F.pullr (∐Fⁿ[⊥].factors _ _) ⟩≡
            α ∘ F.F₁ (Fⁿ[⊥]-fold α j)             ∎)

Furthermore, this extension is unique: this follows from a quick induction paired with the universal property of $F^{\infty }(\perp )\text{.}$

      fold-step
        : ∀ {a} {α : Hom (F.₀ a) a}
        → (f : Hom ∐Fⁿ[⊥] a)
        → f ∘ roll ≡ α ∘ F.₁ f
        → ∀ n → f ∘ ∐Fⁿ[⊥].ψ n ≡ Fⁿ[⊥]-fold α n
      fold-step {α = α} f p zero = sym (¡-unique _)
      fold-step {α = α} f p (suc n) =
         f ∘ ∐Fⁿ[⊥].ψ (suc n)               ≡˘⟨ ap (f ∘_) (F[∐Fⁿ[⊥]].factors _ _) ⟩≡˘
         f ∘ roll ∘ F.F₁ (∐Fⁿ[⊥].ψ n)       ≡⟨ pulll p ⟩≡
         (α ∘ F.F₁ f) ∘ F.F₁ (∐Fⁿ[⊥].ψ n)   ≡⟨ F.pullr (fold-step f p n) ⟩≡
         α ∘ F.₁ (Fⁿ[⊥]-fold _ n)           ∎

      fold-unique
        : ∀ {a} {α : Hom (F.₀ a) a}
        → (f : Hom ∐Fⁿ[⊥] a)
        → f ∘ roll ≡ α ∘ F.₁ f
        → fold α ≡ f
      fold-unique f p = sym $ ∐Fⁿ[⊥].unique _ _ _ (fold-step f p)

If we put all the pieces together, we observe that $(F^{\infty }(\perp ),\mathrm{roll})$ is an initial $F\text{-algebra.}$

      ∐Fⁿ[⊥]-initial : Initial FAlg
      ∐Fⁿ[⊥]-initial .Initial.bot .fst = ∐Fⁿ[⊥]
      ∐Fⁿ[⊥]-initial .Initial.bot .snd = roll
      ∐Fⁿ[⊥]-initial .Initial.has⊥ (a , α) .centre .hom = fold α
      ∐Fⁿ[⊥]-initial .Initial.has⊥ (a , α) .centre .preserves = fold-roll α
      ∐Fⁿ[⊥]-initial .Initial.has⊥ (a , α) .paths f =
        total-hom-path F-Algebras (fold-unique (f .hom) (f .preserves)) prop!

Free algebras and free monads🔗

In the previous section, we dismissed free $F\text{-algebras}$ as somewhat rare objects. It is now time to see why this is the case. Suppose that $\mathcal{C}$ has all free $F\text{-algebras:}$ this is equivalent to requiring a left adjoint to the functor that forgets $F\text{-algebras.}$

  module _ {Free : Functor C FAlg} (Free⊣π : Free ⊣ πᶠ F-Algebras) where
    private
      module Free = Cat.Functor.Reasoning Free
      open _⊣_ Free⊣π
      open Functor

This adjunction induces a monad on $\mathcal{C}\text{,}$ which we will call the algebraically free monad on $F\text{.}$

    Alg-free-monad : Monad C
    Alg-free-monad = Adjunction→Monad Free⊣π

That was pretty abstract, so let’s unpack the data we have on hand. The left adjoint takes each object $A$ to an object $F^{\ast }(A)$ that is equipped with an $F\text{-algebra}$ $\mathrm{roll}:\mathcal{C}(F(F^{\ast }(A)),F^{\ast }(A))\text{.}$

    open Algebra-on {M = Alg-free-monad}

    private
      F* : Ob → Ob
      F* x = Free.₀ x .fst

      roll : ∀ (x : Ob) → Hom (F.₀ (F* x)) (F* x)
      roll x = Free.₀ x .snd

Furthermore, the left adjoint takes each $f:\mathcal{C}(A,B)$ to an $F\text{-algebra}$ homomorphism $F^{\ast }(f)\text{,}$ as in the following diagram:

      map* : ∀ {a b} → Hom a b → Hom (F* a) (F* b)
      map* f = Free.₁ f .hom

      map*-roll : ∀ {a b} (f : Hom a b) → map* f ∘ roll a ≡ roll b ∘ F.₁ (map* f)
      map*-roll f = Free.₁ f .preserves

The counit of our adjunction lets us extend any $F\text{-algebra}$ $\alpha :\mathcal{C}(F(A),A)$ to an $F\text{-algebra}$ $\mathrm{fold}(\alpha ):\mathcal{C}(F^{\ast }(A),A)\text{.}$ Intuitively, this operation lets us eliminate out of the fixpoint by describing how to eliminate out of each layer.

      fold : ∀ {a} → Hom (F.₀ a) a → Hom (F* a) a
      fold {a} α = counit.ε (a , α) .hom

      fold-roll : ∀ {a} (α : Hom (F.₀ a) a) → fold α ∘ roll a ≡ α ∘ F.₁ (fold α)
      fold-roll {a} α = counit.ε (a , α) .preserves

Extending $\mathrm{roll}$ gives us the multiplication of the monad.

      mult : ∀ (x : Ob) → Hom (F* (F* x)) (F* x)
      mult x = fold (roll x)

We can also determine the equality of $F\text{-algebra}$ morphisms $\mathcal{C}(F^{\ast }(A),B)$ purely based off of how they behave on points.

      fold-ext
        : ∀ {a b}
        → (f g : FAlg.Hom (Free.₀ a) b)
        → (f .hom ∘ unit.η _ ≡ g .hom ∘ unit.η _)
        → f .hom ≡ g .hom
      fold-ext f g p =
        ap hom $ Equiv.injective (_ , L-adjunct-is-equiv Free⊣π) {x = f} {y = g} $
        p

Note that any $F\text{-algebra}$ $\alpha :\mathcal{C}(F(A),A)$ yields an algebra for the algebraically free monad via extension along $\mathrm{fold}\text{.}$

    lift-alg : ∀ {a} → Hom (F.₀ a) a → Algebra-on C Alg-free-monad a
    lift-alg {a = a} α .ν = fold α
    lift-alg {a = a} α .ν-unit = zag
    lift-alg {a = a} α .ν-mult =
      ap hom $ counit.is-natural (Free.₀ a) (a , α) (counit.ε (a , α))

Likewise, we can extract an $F\text{-algebra}$ out of a monad algebra by precomposing with $\mathrm{roll}\circ F(\eta )\text{:}$ intuitively, this lifts $F(A)$ into $F^{\ast }(A)$ by adding on zero extra layers, and then passes it off to the monad algebra to be eliminated.

    lower-alg : ∀ {a} → Algebra-on C Alg-free-monad a → Hom (F.₀ a) a
    lower-alg {a = a} α = α .ν ∘ roll a ∘ F.₁ (unit.η a)

We can also view a monad algebra $\alpha$ as a morphism of $F\text{-algebras,}$ as described in the following digram:

This diagram states that we should be able to eliminate a $F(F^{\ast }(A))$ either by rolling in the $F$ and passing the resulting $F^{\ast }(A)$ off to the monad algebra, or by eliminating the inner $F^{\ast }(A)$ first, and then evaluating the remaining $F(A)\text{.}$ Intuitively, this is quite clear, but proving it involves quite a bit of algebra.

    alg*
      : ∀ {a} → (α : Algebra-on C Alg-free-monad a)
      → FAlg.Hom (F* a , roll a) (a , (α .ν ∘ roll a ∘ F.₁ (unit.η a)))
    alg* {a = a} α .hom = α .ν
    alg* {a = a} α .preserves =
      α .ν ∘ roll a                                            ≡⟨ intror (F.annihilate zag) ⟩≡
      (α .ν ∘ roll a) ∘ (F.₁ (mult a) ∘ F.₁ (unit.η _))        ≡⟨ pull-inner (sym $ fold-roll (roll a)) ⟩≡
      α .ν ∘ (mult a ∘ roll (F* a)) ∘ F.₁ (unit.η _)           ≡⟨ dispersel (sym $ α .ν-mult) ⟩≡
      α .ν ∘ Free.₁ (α .ν) .hom ∘ roll (F* a) ∘ F.₁ (unit.η _) ≡⟨ extend-inner (map*-roll (α .ν)) ⟩≡
      α .ν ∘ roll a ∘ F.₁ (map* (α .ν)) ∘ F.₁ (unit.η _)       ≡⟨ centralizer (F.weave (sym (unit.is-natural _ _ _))) ⟩≡
      α .ν ∘ (roll a ∘ F.₁ (unit.η _)) ∘ F.₁ (α .ν)            ≡⟨ assoc _ _ _ ⟩≡
      (α .ν ∘ roll a ∘ F.₁ (unit.η _)) ∘ F.₁ (α .ν)            ∎

However, this algebra pays off, as it lets us establish an equivalence between $F\text{-algebras}$ and algebras over the algebraically free monad on $F\text{.}$

    f-algebra≃free-monad-algebra : ∀ a → Hom (F.₀ a) a ≃ Algebra-on C Alg-free-monad a
    f-algebra≃free-monad-algebra a = Iso→Equiv $
      lift-alg , iso lower-alg
        (Algebra-on-pathp C refl ⊙ equivl)
        equivr
      where
        equivl
          : ∀ {a} (α : Algebra-on C Alg-free-monad a)
          → counit.ε (a , lower-alg α) .hom ≡ α .ν
        equivl α =
          fold-ext (counit.ε _) (alg* α) $ zag ∙ sym (α .ν-unit)

        equivr
          : ∀ {a} (α : Hom (F.₀ a) a)
          → counit.ε (a , α) .hom ∘ roll a ∘ F.₁ (unit.η _) ≡ α
        equivr {a} α =
          pulll (counit.ε (a , α) .preserves) ∙ F.cancelr zag

Likewise, we have an equivalence between $F\text{-algebra}$ morphisms and monad algebra morphisms.

    private module Free-EM = Cat.Reasoning (Eilenberg-Moore Alg-free-monad)

    lift-alg-hom
      : ∀ {a b} {α β}
      → FAlg.Hom (a , α) (b , β)
      → Free-EM.Hom (a , lift-alg α) (b , lift-alg β)
    lift-alg-hom f .hom = f .hom
    lift-alg-hom f .preserves =
      (sym $ ap hom $ counit.is-natural _ _ f)

    lower-alg-hom
      : ∀ {a b} {α β}
      → Free-EM.Hom (a , lift-alg α) (b , lift-alg β)
      → FAlg.Hom (a , α) (b , β)
    lower-alg-hom f .hom = f .hom
    lower-alg-hom {a} {b} {α} {β} f .preserves =
      f .hom ∘ α                                                      ≡⟨ ap₂ _∘_ refl (insertr (F.annihilate zag)) ⟩≡
      f .hom ∘ (α ∘ F.₁ (ε (a , α) .hom)) ∘ F.₁ (η a)                 ≡⟨ push-inner (sym (fold-roll α)) ⟩≡
      ⌜ f .hom ∘ ε (a , α) .hom ⌝ ∘ (roll a ∘ F.₁ (η a))              ≡⟨ ap! (f .preserves) ⟩≡
      (ε (b , β) .hom ∘ Free.F₁ (f .hom) .hom) ∘ (roll a ∘ F.₁ (η a)) ≡⟨ pull-inner (map*-roll (f .hom)) ⟩≡
      ε (b , β) .hom ∘ (roll b ∘ F.₁ (map* (f .hom))) ∘ F.₁ (η a)     ≡⟨ disperse (fold-roll β) (F.weave (sym (unit.is-natural _ _ _))) ⟩≡
      β ∘ F.₁ (ε (b , β) .hom) ∘ F.₁ (η b) ∘ F.₁ (f .hom)             ≡⟨ ap₂ _∘_ refl (cancell (F.annihilate zag)) ⟩≡
      β ∘ (F.₁ (f .hom))                                              ∎

Therefore, we have an isomorphism of precategories between the category of $F\text{-algebras}$ and the Eilenberg-Moore category of the monad we constructed, giving us the appropriate universal property for an algebraically free monad.

    FAlg→Free-EM
      : Functor FAlg (Eilenberg-Moore Alg-free-monad)
    FAlg→Free-EM .F₀ (a , α) =
      a , lift-alg α
    FAlg→Free-EM .F₁ = lift-alg-hom
    FAlg→Free-EM .F-id = ext refl
    FAlg→Free-EM .F-∘ f g = ext refl

    FAlg≅Free-EM : is-precat-iso FAlg→Free-EM
    FAlg≅Free-EM .is-precat-iso.has-is-ff =
      is-iso→is-equiv $ iso lower-alg-hom
        (λ _ → trivial!)
        (λ _ → total-hom-path F-Algebras refl prop!)
    FAlg≅Free-EM .is-precat-iso.has-is-iso =
      Σ-ap-snd f-algebra≃free-monad-algebra .snd

Free algebras and free relative monads🔗

The previous construction of the algebraically free monad on $F$ only works if we have all free $F\text{-algebras.}$ This is a rather strong condition on $F\text{:}$ what can we do in the general setting?

First, note that the category of objects equipped with free $F\text{-algebras}$ forms a full subcategory of $\mathcal{C}\text{.}$

  Free-algebras : Precategory _ _
  Free-algebras = Restrict {C = C} (Free-object (πᶠ F-Algebras))

  Free-algebras↪C : Functor Free-algebras C
  Free-algebras↪C = Forget-full-subcat

  private module Free-algebras = Cat.Reasoning Free-algebras
  module Free-alg (α : Free-algebras.Ob) where
    -- Rexport stuff in a more user-friendly format
    open Free-object (α .snd) public

    ob : Ob
    ob = free .fst

    alg : Hom (F.₀ ob) ob
    alg = free .snd

  open Relative-extension-system

If we restrict along the inclusion from this category, we can construct the free relative extension system on $F\text{.}$ Unlike the algebraically free monad on $F\text{,}$ this extension system always exists, though it may be trivial if $F$ lacks any free algebras.

  Free-relative-extension : Relative-extension-system Free-algebras↪C
  Free-relative-extension .M₀ α =
    Free-alg.ob α
  Free-relative-extension .unit {α} =
    Free-alg.unit α
  Free-relative-extension .bind {α} {β} f =
    Free-alg.fold α {Free-alg.free β} f .hom
  Free-relative-extension .bind-unit-id {α} =
    ap hom $ Free-alg.fold-unit α
  Free-relative-extension .bind-unit-∘ {α} {β} f =
    Free-alg.commute α
  Free-relative-extension .bind-∘ {α} {β} {γ} f g = ap hom $
    Free-alg.fold β f FAlg.∘ Free-alg.fold α g   ≡˘⟨ Free-alg.fold-natural α (Free-alg.fold β f) g ⟩≡˘
    Free-alg.fold α (Free-alg.fold β f .hom ∘ g) ∎