open import Algebra.Semigroup open import Algebra.Monoid open import Algebra.Magma open import Cat.Displayed.Univalence.Thin open import Cat.Functor.Adjoint.Monadic open import Cat.Functor.Equivalence open import Cat.Instances.Delooping open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Prelude open import Data.List module Algebra.Monoid.Category where

# Category of monoidsπ

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 : β {β} {x y : Monoid β} {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 $\id{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 \id{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 Y 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 open import Cat.Diagram.Monad hiding (Freeβ£Forget) 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)