module Cat.Functor.Algebra where
module _ {o } {C : Precategory o } (F : Functor C C) where

Algebras over an endofunctor🔗

Let be an arbitrary endofunctor on We can view as a means of embellishing an object with extra structure: for instance, the functor endows with an additional point and an endomap the functor adds an extra point and a copy of etc. Consequently, a map picks out a suitably structured e.g. writing a map requires to be equipped with a global element and an endomap In analogy to monad algebras, a map is called an F-algebra on 1.

Likewise, a map between two and is an F-algebra homomorphism if it commutes with the algebras on and as in the following digram.

Intuitively, morphisms are morphisms that preserve the structure encoded by going back to our previous example, an homomorphism between and is a map that preserves the designated global elements of and and commutes with the chosen endomaps.

We can assemble into a displayed category over the type of objects over consists of all possible algebra structures on and the type of morphisms over are proofs that is an 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 2
  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

  FAlg : Precategory (o  ) 
  FAlg =  F-Algebras

  module FAlg = Cat.Reasoning FAlg

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

Lambek’s lemma🔗

As noted above, are a tool for picking out objects equipped with a semantics for a “signature” described by This leads to a very natural question: can we characterize the syntax generated from the signature of

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 for now: free objects are much harder to come by, and initial 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 be an and note that is also an If has a section then and are 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 

On to the main result. Let be an initial As before, is also an so initiality gives us a unique morphism Likewise, induces an morphism Furthermore, is a section of as maps out of the initial object are unique. Therefore, must also be an inverse, so 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
      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)

This result means that an initial is a fixpoint of the functor and should be thought of as the the object The canonical example is the initial algebra of if it exists, this will be an object of the form in this initial algebra is the natural numbers! In general, initial are how we give a categorical semantics to non-indexed inductive datatypes like Nat or List.

Adámek’s fixpoint theorem🔗

Note that initial need not exist for a given functor Nevertheless, Adámek’s fixpoint theorem lets us construct some initial provided that:

  1. has an initial object.
  2. has a colimit for the diagram:
  1. 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 where is the poset of natural numbers, regarded as a category.

    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
Functoriality follows from some straightforward induction.
    Fⁿ[⊥]-id :  n  F₁ⁿ[⊥] (≤-refl {n})  id
    Fⁿ[⊥]-id zero = ¡-unique id
    Fⁿ[⊥]-id (suc n) = F.elim (Fⁿ[⊥]-id n)

      :  {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 can be extended to a morphism Furthermore, this extension is natural in

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

      :  {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 has a colimit of the diagram and preserves this colimit. We can equip with an by using the universal property of the colimit

    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 to a morphism by using the universal property, along with the extensions we constructed earlier.

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

This extension commutes with and thus induces an morphism

      fold-roll :  {a} (α : Hom (F.₀ a) a)  fold α  roll  α  F.₁ (fold α)
      fold-roll α =
        F[∐Fⁿ[⊥]].unique₂ (Fⁿ[⊥]-fold α  suc) (Fⁿ[⊥]-fold-nat  s≤s)
            (fold α  roll)  F.₁ (∐Fⁿ[⊥].ψ j) ≡⟨ pullr (F[∐Fⁿ[⊥]].factors _ _) 
            fold α  ∐Fⁿ[⊥].ψ (suc j)          ≡⟨ ∐Fⁿ[⊥].factors _ _ 
            Fⁿ[⊥]-fold α (suc 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

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

        :  {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 is an initial

      ∐Fⁿ[⊥]-initial : Initial FAlg
      ∐Fⁿ[⊥]-initial .fst = ∐Fⁿ[⊥]
      ∐Fⁿ[⊥]-initial .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 as somewhat rare objects. It is now time to see why this is the case. Suppose that has all free this is equivalent to requiring a left adjoint to the functor that forgets

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

This adjunction induces a monad on which we will call the algebraically free monad on

    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 to an object that is equipped with an

      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 to an homomorphism 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 to an 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 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 morphisms purely based off of how they behave on points.

        :  {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} $

Note that any yields an algebra for the algebraically free monad via extension along

    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 $ (Free.₀ a) (a , α) (counit.ε (a , α))

Likewise, we can extract an out of a monad algebra by precomposing with intuitively, this lifts into 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 as a morphism of as described in the following digram:

This diagram states that we should be able to eliminate a either by rolling in the and passing the resulting off to the monad algebra, or by eliminating the inner first, and then evaluating the remaining Intuitively, this is quite clear, but proving it involves quite a bit of algebra.

      :  {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 ( _ _ _))) 
      α .ν  (roll a  F.₁ (unit.η _))  F.₁ (α .ν)            ≡⟨ assoc _ _ _ 
      (α .ν  roll a  F.₁ (unit.η _))  F.₁ (α .ν)            

However, this algebra pays off, as it lets us establish an equivalence between and algebras over the algebraically free monad on

    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)
          :  {a} (α : Algebra-on C Alg-free-monad a)
           counit.ε (a , lower-alg α) .hom  α .ν
        equivl α =
          fold-ext (counit.ε _) (alg* α) $ zag  sym (α .ν-unit)

          :  {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 morphisms and monad algebra morphisms.

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

      :  {a b} {α β}
       FAlg.Hom (a , α) (b , β)
       Free-EM.Hom (a , lift-alg α) (b , lift-alg β)
    lift-alg-hom f .morphism = f .hom
    lift-alg-hom f .commutes =
      (sym $ ap hom $ _ _ f)

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

Therefore, we have an isomorphism of precategories between the category of and the Eilenberg-Moore category of the monad we constructed, giving us the appropriate universal property for an algebraically free monad.

      : Functor FAlg (Eilenberg-Moore C 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 only works if we have all free This is a rather strong condition on what can we do in the general setting?

First, note that the category of objects equipped with free forms a full subcategory of

  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

If we restrict along the inclusion from this category, we can construct the free relative extension system on Unlike the algebraically free monad on this extension system always exists, though it may be trivial if 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 α { β} 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) 

  1. Alternatively, we can view as monad algebras over functors that lack algebraic structure.↩︎