module Algebra.Monoid.Category where

open Precategory open is-semigroup open is-magma open Monoid-hom open Monoid-on open Functor open _=>_ open _β£_ private map : β {β β'} {A : Type β} {B : Type β'} β (A β B) β List A β List B map = Meta.Idiom.map

# Category of monoidsπ

The collection of all `Monoid`

s 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.

MonβͺSets : β {β} β Functor (Monoids β) (Sets β) MonβͺSets = Forget-structure (Monoid-structure _)

## Free objectsπ

We piece together some properties of `lists`

to show that, if
$A$
is a set, then
$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β¦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.

Free-monoid : β {β} β Functor (Sets β) (Monoids β) Free-monoid .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-monoid .Fβ f = total-hom (map f) record { pres-id = refl ; pres-β = map-++ f } Free-monoid .F-id = ext map-id Free-monoid .F-β f g = ext 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-monoidβ£Forget : β {β} β Free-monoid {β} β£ MonβͺSets Free-monoidβ£Forget .unit .Ξ· _ x = x β· [] Free-monoidβ£Forget .unit .is-natural x y f = refl Free-monoidβ£Forget .counit .Ξ· M = total-hom (fold _) record { pres-id = refl ; pres-β = fold-++ } Free-monoidβ£Forget .counit .is-natural x y th = ext $ fold-natural (th .hom) (th .preserves) Free-monoidβ£Forget .zig {A = A} = ext $ fold-pure {X = A} Free-monoidβ£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-monoidβ£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-monoidβ£Forget {β}) Monoid-is-monadic {β} = ff+split-esoβis-equivalence it's-ff it's-eso where open import Cat.Diagram.Monad comparison = Comparison-EM (Free-monoidβ£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 .hom from alg .preserves .pres-id = happly (alg .preserves) [] 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 .preserves 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 .hom

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 = trivial! toβfrom : is-left-inverse from comparison.β toβfrom x = trivial!

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β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 import Cat.Reasoning (Eilenberg-Moore (LβR (Free-monoidβ£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 .hom = Ξ» x β x into .preserves = funext (Ξ» x β recover x β ap (alg .Ξ½) (sym (map-id x))) from : Algebra-hom _ (A , alg) (comparison.β monoid) from .hom = Ξ» x β x from .preserves = 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 trivial! trivial!