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.

Forget : βˆ€ {β„“} β†’ Functor (Monoids β„“) (Sets β„“)
Forget = 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 : βˆ€ {β„“} β†’ 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 = ext map-id
Free .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⊣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 =
  ext $ fold-natural (th .hom) (th .preserves)
Free⊣Forget .zig {A = A} =
  ext $ 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 = 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
    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)