module Algebra.Monoid.Category where

open Precategory open is-semigroup open is-monoid 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 monoidsð

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!