open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Magma

open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
open import Cat.Prelude

open import Data.List

module Algebra.Monoid.Category where

open Precategory
open is-semigroup
open is-magma
open Monoid-hom
open Monoid-on
open Functor
open _=>_
open _β£_


# Category of monoidsπ

_ = is-prop


The collection of all Monoids relative to some universe level assembles into a precategory. This is because being a monoid homomorphism is a proposition, and so does not raise the h-level of the Hom-sets.

instance
H-Level-Monoid-hom
: β {β ββ²} {s : Type β} {t : Type ββ²}
β β {x : Monoid-on s} {y : Monoid-on t} {f} {n}
β H-Level (Monoid-hom x y f) (suc n)
H-Level-Monoid-hom {y = M} = prop-instance Ξ» x y i β
record { pres-id = M .has-is-set _ _ (x .pres-id) (y .pres-id) i
; pres-β = Ξ» a b β M .has-is-set _ _ (x .pres-β a b) (y .pres-β a b) i
}


Itβs routine to check that the identity is a monoid homomorphism and that composites of homomorphisms are again homomorphisms; This means that Monoid-on assembles into a structure thinly displayed over the category of sets, so that we may appeal to general results about displayed categories to reason about the category of monoids.

Monoid-structure : β β β Thin-structure β Monoid-on
Monoid-structure β .is-hom f A B = el! $Monoid-hom A B f Monoid-structure β .id-is-hom .pres-id = refl Monoid-structure β .id-is-hom .pres-β x y = refl Monoid-structure β .β-is-hom f g p1 p2 .pres-id = ap f (p2 .pres-id) β p1 .pres-id Monoid-structure β .β-is-hom f g p1 p2 .pres-β x y = ap f (p2 .pres-β _ _) β p1 .pres-β _ _ Monoid-structure β .id-hom-unique mh _ i .identity = mh .pres-id i Monoid-structure β .id-hom-unique mh _ i ._β_ x y = mh .pres-β x y i Monoid-structure β .id-hom-unique {s = s} {t = t} mh _ i .has-is-monoid = is-propβpathp (Ξ» i β hlevel {T = is-monoid (mh .pres-id i) (Ξ» x y β mh .pres-β x y i)} 1) (s .has-is-monoid) (t .has-is-monoid) i Monoids : β β β Precategory (lsuc β) β Monoids β = Structured-objects (Monoid-structure β) Monoids-is-category : β {β} β is-category (Monoids β) Monoids-is-category = Structured-objects-is-category (Monoid-structure _)  By standard nonsense, then, the category of monoids admits a faithful functor into the category of sets. Forget : β {β} β Functor (Monoids β) (Sets β) Forget = Forget-structure (Monoid-structure _)  ## Free objectsπ We piece together some properties of lists to show that, if $A$ is a set, then $\mathrm{List}(A)$ is an object of Monoids; The operation is list concatenation, and the identity element is the empty list. List-is-monoid : β {β} {A : Type β} β is-set A β Monoid-on (List A) List-is-monoid aset .identity = [] List-is-monoid aset ._β_ = _++_ List-is-monoid aset .has-is-monoid .idl = refl List-is-monoid aset .has-is-monoid .idr = ++-idr _ List-is-monoid aset .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set = ListPath.is-setβList-is-set aset List-is-monoid aset .has-is-monoid .has-is-semigroup .associative {x} {y} {z} = sym (++-assoc x y z)  We prove that the assignment $X \mapsto \mathrm{List}(X)$ is functorial; We call this functor Free, since it is a left adjoint to the Forget functor defined above: it solves the problem of turning a set into a monoid in the most efficient way. map-id : β {β} {A : Type β} (xs : List A) β map (Ξ» x β x) xs β‘ xs map-id [] = refl map-id (x β· xs) = ap (x β·_) (map-id xs) map-++ : β {β} {x y : Type β} (f : x β y) xs ys β map f (xs ++ ys) β‘ map f xs ++ map f ys map-++ f [] ys = refl map-++ f (x β· xs) ys = ap (f x β·_) (map-++ f xs ys) Free : β {β} β Functor (Sets β) (Monoids β) Free .Fβ A = el! (List β£ A β£) , List-is-monoid (A .is-tr)  The action on morphisms is given by map, which preserves the monoid identity definitionally; We must prove that it preserves concatenation, identity and composition by induction on the list. Free .Fβ f = total-hom (map f) record { pres-id = refl ; pres-β = map-++ f } Free .F-id = Homomorphism-path map-id Free .F-β f g = Homomorphism-path map-β where map-β : β xs β map (Ξ» x β f (g x)) xs β‘ map f (map g xs) map-β [] = refl map-β (x β· xs) = ap (f (g x) β·_) (map-β xs)  We refer to the adjunction counit as fold, since it has the effect of multiplying all the elements in the list together. It βfoldsβ it up into a single value. fold : β {β} (X : Monoid β) β List (X .fst) β X .fst fold (M , m) = go where module M = Monoid-on m go : List M β M go [] = M.identity go (x β· xs) = x M.β go xs  We prove that fold is a monoid homomorphism, and that it is a natural transformation, hence worthy of being an adjunction counit. fold-++ : β {β} {X : Monoid β} (xs ys : List (X .fst)) β fold X (xs ++ ys) β‘ Monoid-on._β_ (X .snd) (fold X xs) (fold X ys) fold-++ {X = X} = go where module M = Monoid-on (X .snd) go : β xs ys β _ go [] ys = sym M.idl go (x β· xs) ys = fold X (x β· xs ++ ys) β‘β¨β© x M.β fold X (xs ++ ys) β‘β¨ ap (_ M.β_) (go xs ys) β©β‘ x M.β (fold X xs M.β fold X ys) β‘β¨ M.associative β©β‘ fold X (x β· xs) M.β fold X ys β fold-natural : β {β} {X Y : Monoid β} f β Monoid-hom (X .snd) (Y .snd) f β β xs β fold Y (map f xs) β‘ f (fold X xs) fold-natural f mh [] = sym (mh .pres-id) fold-natural {X = X} {Y} f mh (x β· xs) = f x Y.β fold Y (map f xs) β‘β¨ ap (_ Y.β_) (fold-natural f mh xs) β©β‘ f x Y.β f (fold X xs) β‘β¨ sym (mh .pres-β _ _) β©β‘ f (x X.β fold X xs) β where module X = Monoid-on (X .snd) module Y = Monoid-on (Y .snd)  Proving that it satisfies the zig triangle identity is the lemma fold-pure below. fold-pure : β {β} {X : Set β} (xs : List β£ X β£) β fold (List β£ X β£ , List-is-monoid (X .is-tr)) (map (Ξ» x β x β· []) xs) β‘ xs fold-pure [] = refl fold-pure {X = X} (x β· xs) = ap (x β·_) (fold-pure {X = X} xs) Freeβ£Forget : β {β} β Free {β} β£ Forget Freeβ£Forget .unit .Ξ· _ x = x β· [] Freeβ£Forget .unit .is-natural x y f = refl Freeβ£Forget .counit .Ξ· M = total-hom (fold _) record { pres-id = refl ; pres-β = fold-++ } Freeβ£Forget .counit .is-natural x y th = Homomorphism-path$ fold-natural (th .hom) (th .preserves)
Freeβ£Forget .zig {A = A} =
Homomorphism-path \$ fold-pure {X = A}
Freeβ£Forget .zag {B = B} i x = B .snd .idr {x = x} i


This concludes the proof that Monoids has free objects. We now prove that monoids are equivalently algebras for the List monad, i.e.Β that the Freeβ£Forget adjunction is monadic. More specifically, we show that the canonically-defined comparison functor is fully faithful (list algebra homomoprhisms are equivalent to monoid homomorphisms) and that it is split essentially surjective.

Monoid-is-monadic : β {β} β is-monadic (Freeβ£Forget {β})
Monoid-is-monadic {β} = ff+split-esoβis-equivalence it's-ff it's-eso where

comparison = Comparison (Freeβ£Forget {β})
module comparison = Functor comparison

it's-ff : is-fully-faithful comparison
it's-ff {x} {y} = is-isoβis-equiv (iso from fromβto toβfrom) where
module x = Monoid-on (x .snd)
module y = Monoid-on (y .snd)


First, for full-faithfulness, it suffices to prove that the morphism part of comparison is an isomorphism. Hence, define an inverse; It suffices to show that the underlying map of the algebra homomorphism is a monoid homomorphism, which follows from the properties of monoids:

    from : Algebra-hom _ _ (comparison.β x) (comparison.β y) β Monoids β .Hom x y
from alg .hom = alg .Algebra-hom.morphism
from alg .preserves .pres-id = happly (alg .Algebra-hom.commutes) []
from alg .preserves .pres-β a b =
f (a x.β b)                  β‘Λβ¨ ap f (ap (a x.β_) x.idr) β©β‘Λ
f (a x.β (b x.β x.identity)) β‘β¨ (Ξ» i β alg .Algebra-hom.commutes i (a β· b β· [])) β©β‘
f a y.β (f b y.β y.identity) β‘β¨ ap (f a y.β_) y.idr β©β‘
f a y.β f b                  β
where f = alg .Algebra-hom.morphism


The proofs that this is a quasi-inverse is immediate, since both βbeing an algebra homomorphismβ and βbeing a monoid homomorphismβ are properties of the underlying map.

    fromβto : is-right-inverse from comparison.β
fromβto x = Algebra-hom-path _ refl

toβfrom : is-left-inverse from comparison.β
toβfrom x = Homomorphism-path Ξ» _ β refl


Showing that the functor is essentially surjective is significantly more complicated. We must show that we can recover a monoid from a List algebra (a βfoldβ): We take the unit element to be the fold of the empty list, and the binary operation $x \star y$ to be the fold of the list $[x,y]$.

  it's-eso : is-split-eso comparison
it's-eso (A , alg) = monoid , the-iso where
open Algebra-on
open Algebra-hom
import Cat.Reasoning (Eilenberg-Moore _ (LβR (Freeβ£Forget {β}))) as R

monoid : Monoids β .Ob
monoid .fst = A
monoid .snd .identity = alg .Ξ½ []
monoid .snd ._β_ a b = alg .Ξ½ (a β· b β· [])


It suffices, through incredibly tedious calculations, to show that these data assembles into a monoid:

    monoid .snd .has-is-monoid = has-is-m where abstract
has-is-m : is-monoid (alg .Ξ½ []) (monoid .snd ._β_)
has-is-m .has-is-semigroup = record
{ has-is-magma = record { has-is-set = A .is-tr }
; associative  = Ξ» {x} {y} {z} β
alg .Ξ½ (β x β β· alg .Ξ½ (y β· z β· []) β· [])               β‘Λβ¨ apΒ‘ (happly (alg .Ξ½-unit) x) β©β‘Λ
alg .Ξ½ (alg .Ξ½ (x β· []) β· alg .Ξ½ (y β· z β· []) β· [])     β‘β¨ happly (alg .Ξ½-mult) _ β©β‘
alg .Ξ½ (x β· y β· z β· [])                                 β‘Λβ¨ happly (alg .Ξ½-mult) _ β©β‘Λ
alg .Ξ½ (alg .Ξ½ (x β· y β· []) β· β alg .Ξ½ (z β· []) β β· []) β‘β¨ ap! (happly (alg .Ξ½-unit) z) β©β‘
alg .Ξ½ (alg .Ξ½ (x β· y β· []) β· z β· [])                   β
}
has-is-m .idl {x} =
alg .Ξ½ (alg .Ξ½ [] β· β x β β· [])            β‘Λβ¨ apΒ‘ (happly (alg .Ξ½-unit) x) β©β‘Λ
alg .Ξ½ (alg .Ξ½ [] β· alg .Ξ½ (x β· []) β· [])  β‘β¨ happly (alg .Ξ½-mult) _ β©β‘
alg .Ξ½ (x β· [])                            β‘β¨ happly (alg .Ξ½-unit) x β©β‘
x                                          β
has-is-m .idr {x} =
alg .Ξ½ (β x β β· alg .Ξ½ [] β· [])            β‘Λβ¨ apΒ‘ (happly (alg .Ξ½-unit) x) β©β‘Λ
alg .Ξ½ (alg .Ξ½ (x β· []) β· alg .Ξ½ [] β· [])  β‘β¨ happly (alg .Ξ½-mult) _ β©β‘
alg .Ξ½ (x β· [])                            β‘β¨ happly (alg .Ξ½-unit) x β©β‘
x                                          β


The most important lemma is that folding a list using this monoid recovers the original algebra multiplication, which we can show by induction on the list:

    recover : β x β fold _ x β‘ alg .Ξ½ x
recover []       = refl
recover (x β· xs) =
alg .Ξ½ (x β· fold _ xs β· [])               β‘β¨ apβ (Ξ» e f β alg .Ξ½ (e β· f β· [])) (sym (happly (alg .Ξ½-unit) x)) (recover xs) β©β‘
alg .Ξ½ (alg .Ξ½ (x β· []) β· alg .Ξ½ xs β· []) β‘β¨ happly (alg .Ξ½-mult) _ β©β‘
alg .Ξ½ (x β· xs ++ [])                     β‘β¨ ap (alg .Ξ½) (++-idr _) β©β‘
alg .Ξ½ (x β· xs)                           β


We must then show that the image of this monoid under Comparison is isomorphic to the original algebra. Fortunately, this follows from the recover lemma above; The isomorphism itself is given by the identity function in both directions, since the recovered monoid has the same underlying type as the List-algebra!

    into : Algebra-hom _ _ (comparison.β monoid) (A , alg)
into .morphism = Ξ» x β x
into .commutes = funext (Ξ» x β recover x β ap (alg .Ξ½) (sym (map-id x)))

from : Algebra-hom _ _ (A , alg) (comparison.β monoid)
from .morphism = Ξ» x β x
from .commutes =
funext (Ξ» x β sym (recover x) β ap (fold _) (sym (map-id x)))

the-iso : comparison.β monoid R.β (A , alg)
the-iso = R.make-iso into from (Algebra-hom-path _ refl) (Algebra-hom-path _ refl)