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-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🔗

_ = 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 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!