Library UniMath.Algebra.Universal.Examples.Monoid
Example on monoids.
Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021Require Import UniMath.MoreFoundations.Notations.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Universal.EqAlgebras.
Local Open Scope stn.
Local Open Scope eq.
Signature.
Definition monoid_signature := make_signature_simple_single_sorted [2; 0].
Definition monoid_sort : sorts monoid_signature := tt.
Algebra of monoids without equations.
Definition monoid_algebra (M: monoid)
: algebra monoid_signature
:= make_algebra_simple_single_sorted' monoid_signature M [( op ; unel M )].
Module Eqspec.
Free algebra of open terms.
Definition monoid_varspec : varspec monoid_signature
:= make_varspec monoid_signature natset (λ _, monoid_sort).
Definition Mon : UU := term monoid_signature monoid_varspec tt.
Definition mul : Mon → Mon → Mon := build_term' (●0: names monoid_signature).
Definition id : Mon := build_term' (●1: names monoid_signature).
Definition x : Mon := varterm (0: monoid_varspec).
Definition y : Mon := varterm (1: monoid_varspec).
Definition z : Mon := varterm (2: monoid_varspec).
Definition monoid_mul_assoc := mul (mul x y) z == mul x (mul y z).
Definition monoid_mul_lid := mul id x == x.
Definition monoid_mul_rid := mul x id == x.
Definition monoid_axioms : eqsystem monoid_signature monoid_varspec
:= ⟦ 3 ⟧,, three_rec monoid_mul_assoc monoid_mul_lid monoid_mul_rid.
Definition monoid_eqspec : eqspec.
Proof.
use tpair. { exact monoid_signature. }
use tpair. { exact monoid_varspec. }
exact monoid_axioms.
Defined.
Definition monoid_eqalgebra := eqalgebra monoid_eqspec.
Every monoid is a monoid eqalgebra.
Section Make_Monoid_Eqalgebra.
Variable M : monoid.
Lemma holds_monoid_mul_lid : holds (monoid_algebra M) monoid_mul_lid.
Proof.
intro. cbn in α.
change (fromterm (ops (monoid_algebra M)) α tt (mul id x) = α 0).
change (op (unel M) (α 0) = α 0).
apply lunax.
Qed.
Lemma holds_monoid_mul_rid : holds (monoid_algebra M) monoid_mul_rid.
Proof.
intro.
change (op (α 0) (unel M) = α 0).
apply runax.
Qed.
Lemma holds_monoid_mul_assoc : holds (monoid_algebra M) monoid_mul_assoc.
Proof.
intro.
change (op (op (α 0) (α 1)) (α 2) = op (α 0) (op (α 1) (α 2))).
apply assocax.
Qed.
Definition is_eqalgebra_monoid :
is_eqalgebra (σ := monoid_eqspec) (monoid_algebra M).
Proof.
red. simpl.
apply three_rec_dep; cbn.
- exact holds_monoid_mul_assoc.
- exact holds_monoid_mul_lid.
- exact holds_monoid_mul_rid.
Defined.
Definition make_monoid_eqalgebra : monoid_eqalgebra.
use make_eqalgebra.
- exact (monoid_algebra M).
- exact is_eqalgebra_monoid.
Defined.
End Make_Monoid_Eqalgebra.
End Eqspec.