open import Algebra.Semigroup open import Algebra.Monoid open import Algebra.Magma open import Cat.Functor.Adjoint.Monadic open import Cat.Functor.Equivalence open import Cat.Instances.Delooping open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Prelude open import Data.List 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 : ∀ {ℓ} {x y : Monoid ℓ} {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 } Monoids : ∀ ℓ → Precategory (lsuc ℓ) ℓ Monoids ℓ .Ob = Monoid ℓ Monoids ℓ .Hom A B = Σ (Monoid-hom A B) Monoids ℓ .Hom-set _ (_ , M) = hlevel 2 where open Monoid-on M
It’s routine to check that the identity is a monoid homomorphism and that composites of homomorphisms are again homomorphisms.
Monoids ℓ .id = (λ x → x) , record { pres-id = refl ; pres-⋆ = λ _ _ → refl } Monoids ℓ ._∘_ (f , fh) (g , gh) = f ⊙ g , fogh where fogh : Monoid-hom _ _ (f ⊙ g) fogh .pres-id = ap f (gh .pres-id) ∙ fh .pres-id fogh .pres-⋆ x y = ap f (gh .pres-⋆ x y) ∙ fh .pres-⋆ _ _ Monoids ℓ .idr f = Σ-prop-path (λ _ → hlevel 1) refl Monoids ℓ .idl f = Σ-prop-path (λ _ → hlevel 1) refl Monoids ℓ .assoc f g h = Σ-prop-path (λ _ → hlevel 1) refl
The category of monoids admits a faithful functor to the category of sets: Forget.
Forget : ∀ {ℓ} → Functor (Monoids ℓ) (Sets ℓ) Forget .F₀ (A , m) = A , m .has-is-set Forget .F₁ = fst Forget .F-id = refl Forget .F-∘ _ _ = refl
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.
map-id : ∀ {ℓ} {A : Type ℓ} (xs : List A) → map (λ x → x) xs ≡ xs map-id [] = refl map-id (x ∷ xs) = ap (x ∷_) (map-id xs) map-++ : ∀ {ℓ} {x y : Type ℓ} (f : x → y) xs ys → map f (xs ++ ys) ≡ map f xs ++ map f ys map-++ f [] ys = refl map-++ f (x ∷ xs) ys = ap (f x ∷_) (map-++ f xs ys) Free : ∀ {ℓ} → Functor (Sets ℓ) (Monoids ℓ) Free .F₀ A = 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 = map f , record { pres-id = refl ; pres-⋆ = map-++ f } Free .F-id = Σ-prop-path (λ _ → hlevel 1) (funext map-id) Free .F-∘ f g = Σ-prop-path (λ _ → hlevel 1) (funext 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 Y 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 = fold M , record { pres-id = refl ; pres-⋆ = fold-++ } Free⊣Forget .counit .is-natural x y (f , h) = Σ-prop-path (λ _ → hlevel 1) (funext (fold-natural {X = x} {y} f h)) Free⊣Forget .zig {A = A} = Σ-prop-path (λ _ → hlevel 1) (funext (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 .fst = alg .Algebra-hom.morphism from alg .snd .pres-id = happly (alg .Algebra-hom.commutes) [] from alg .snd .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 = Algebra-hom-path _ refl to∘from : is-left-inverse from comparison.₁ to∘from x = Σ-prop-path (λ _ → hlevel 1) refl
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 (λ x → alg .ν (x ∷ _)) (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 (λ x → alg .ν (_ ∷ x ∷ [])) (happly (alg .ν-unit) z) ⟩≡ alg .ν (alg .ν (x ∷ y ∷ []) ∷ z ∷ []) ∎ } has-is-m .idl {x} = alg .ν (alg .ν [] ∷ x ∷ []) ≡˘⟨ ap (λ x → alg .ν (alg .ν [] ∷ x ∷ [])) (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 (λ x → alg .ν (x ∷ _)) (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 monoid x ≡ alg .ν x recover [] = refl recover (x ∷ xs) = alg .ν (x ∷ fold monoid 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 monoid) (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)