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
    :  { ℓ'} {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 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!