open import 1Lab.Prelude

open import Algebra.Semigroup

module Algebra.Monoid where


# Monoidsπ

A monoid is a semigroup equipped with a two-sided identity element: An element $e \in M$ such that $e \star x = x = x \star e$. For any particular choice of binary operator $\star$, if a two-sided identity exists, then it is unique; In this sense, βbeing a monoidβ could be considered an βaxiomβ that semigroups may satisfy.

However, since semigroup homomorphisms do not automatically preserve the identity element1, it is part of the type signature for is-monoid, being considered structure that a semigroup may be equipped with.

record is-monoid (id : A) (_β_ : A β A β A) : Type (level-of A) where
field
has-is-semigroup : is-semigroup _β_

open is-semigroup has-is-semigroup public

field
idl : {x : A} β id β x β‘ x
idr : {x : A} β x β id β‘ x

open is-monoid public


The condition of $(A, 0, \star)$ defining a monoid is a proposition, so that we may safely decompose monoids as the structure $(0, \star)$, which has to satisfy the property of being a monoid.

private unquoteDecl eqv = declare-record-iso eqv (quote is-monoid)

instance
H-Level-is-monoid : β {id : A} {_β_ : A β A β A} {n}
β H-Level (is-monoid id _β_) (suc n)
H-Level-is-monoid = prop-instance Ξ» x β
let open is-monoid x in is-hlevelβ 1 (IsoβEquiv eqv eβ»ΒΉ) (hlevel 1) x


A monoid structure on a type is given by the choice of identity element, the choice of binary operation, and the witness that these choices form a monoid. A Monoid, then, is a type with a monoid structure.

record Monoid-on (A : Type β) : Type β where
field
identity : A
_β_ : A β A β A

has-is-monoid : is-monoid identity _β_

open is-monoid has-is-monoid public

Monoid : (β : Level) β Type (lsuc β)
Monoid β = Ξ£ (Monoid-on {β = β})

open Monoid-on


There is also a predicate which witnesses when an equivalence between monoids is a monoid homomorphism. It has to preserve the identity, and commute with the multiplication:

record
Monoid-hom (A B : Ξ£ (Monoid-on {β = β})) (e : A .fst β B .fst) : Type β where
private
module A = Monoid-on (A .snd)
module B = Monoid-on (B .snd)

field
pres-id : e A.identity β‘ B.identity
pres-β : (x y : A .fst) β e (x A.β y) β‘ e x B.β e y

open Monoid-hom

Monoidβ : (A B : Ξ£ (Monoid-on {β = β})) (e : A .fst β B .fst) β Type _
Monoidβ A B (e , _) = Monoid-hom A B e


We automatically derive a proof that Monoid-on is univalent for the structure induced by Monoidβ:

Monoid-univalent : is-univalent {β = β} (HomTβStr Monoidβ)
Monoid-univalent {β = β} =
Derive-univalent-record (record-desc
(Monoid-on {β = β}) Monoidβ
(record:
field[ identity    by pres-id ]
field[ _β_         by pres-β ]
axiom[ has-is-monoid by (Ξ» _ β hlevel 1) ]))


From this, we automatically get a specialisation of the SIP for Monoids, which says that identification of monoids is monoid isomorphism.

Monoidβ‘ : {A B : Monoid β} β (A β[ HomTβStr Monoidβ ] B) β (A β‘ B)
Monoidβ‘ = SIP Monoid-univalent


# Relationships to Unital Magmasπ

open import Algebra.Magma.Unital


By definition, every monoid is exactly a unital magma that is also a semigroup. However, adopting this as a definition yields several issues especially when it comes to metaprogramming, which is why this is instead expressed by explicitly proving the implications between the properties.

First, we show that every monoid is a unital magma:

module _ {id : A} {_β_ : A β A β A} where
is-monoidβis-unital-magma : is-monoid id _β_ β is-unital-magma id _β_
is-monoidβis-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma
is-monoidβis-unital-magma mon .idl = mon .idl
is-monoidβis-unital-magma mon .idr = mon .idr


βReshufflingβ the record fields also allows us to show the reverse direction, namely, that every unital semigroup is a monoid.

  is-unital-magmaβis-semigroupβis-monoid
: is-unital-magma id _β_ β is-semigroup _β_ β is-monoid id _β_
is-unital-magmaβis-semigroupβis-monoid uni sem .has-is-semigroup = sem
is-unital-magmaβis-semigroupβis-monoid uni sem .idl = uni .idl
is-unital-magmaβis-semigroupβis-monoid uni sem .idr = uni .idr


# Inversesπ

A useful application of the monoid laws is in showing that having an inverse is a proprety of a specific element, not structure on that element. To make this precise: Let $e$ be an element of a monoid, say $(M, 1, \star)$; If there are $x$ and $y$ such that $x \star e = 1$ and $e \star y = 1$, then $x = y$.

monoid-inverse-unique
: β {1M : A} {_β_ : A β A β A}
β (m : is-monoid 1M _β_)
β (e x y : A)
β (x β e β‘ 1M) β (e β y β‘ 1M)
β x β‘ y


This is a happy theorem where stating the assumptions takes as many lines as the proof, which is a rather boring calculation. Since $1$ is an identity for $\star$, we can freely multiply by $1$ to βsneak inβ a $y$:

monoid-inverse-unique {1M = 1M} {_β_} m e x y li1 ri2 =
x             β‘β¨ sym (m .idr) β©β‘
x β 1M        β‘β¨ apβ _β_ refl (sym ri2) β©β‘
x β (e β y)   β‘β¨ m .associative β©β‘
(x β e) β y   β‘β¨ apβ _β_ li1 refl β©β‘
1M β y        β‘β¨ m .idl β©β‘
y             β


1. Counterexample: The map $f : (\bb{Z}, *) \to (\bb{Z}, *)$ which sends everything to zero is a semigroup homomorphism, but does not preserve the unit of $(\bb{Z}, *)$.β©οΈ