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.Functor.Properties
open import Cat.Functor.Adjoint
open import Cat.Prelude

open import Data.List

import Meta.Idiom

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π

_ = 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. MonβͺSets : β {β} β Functor (Monoids β) (Sets β) MonβͺSets = Forget-structure (Monoid-structure _)  ## Free objectsπ We piece together some properties of lists to show that, if is a set, then 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 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 to be the fold of the list

  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!