Library UniMath.Algebra.Universal.Examples.Monoid

Example on monoids.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021
This file contains the definition of the signature of monoids and the way to turn a monoid (as defined in UniMath.Algebra.Monoids) into an algebra.

Require 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.
Show proof.
  use tpair. { exact monoid_signature. }
  use tpair. { exact monoid_varspec. }
  exact monoid_axioms.

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.
Show proof.
  intro. cbn in α.
  change (fromterm (ops (monoid_algebra M)) α tt (mul id x) = α 0).
  change (op (unel M) (α 0) = α 0).
  apply lunax.

Lemma holds_monoid_mul_rid : holds (monoid_algebra M) monoid_mul_rid.
Show proof.
  intro.
  change (op (α 0) (unel M) = α 0).
  apply runax.

Lemma holds_monoid_mul_assoc : holds (monoid_algebra M) monoid_mul_assoc.
Show proof.
  intro.
  change (op (op (α 0) (α 1)) (α 2) = op (α 0) (op (α 1) (α 2))).
  apply assocax.

Definition is_eqalgebra_monoid :
  is_eqalgebra (σ := monoid_eqspec) (monoid_algebra M).
Show proof.
  red. simpl.
  apply three_rec_dep; cbn.
  - exact holds_monoid_mul_assoc.
  - exact holds_monoid_mul_lid.
  - exact holds_monoid_mul_rid.

Definition make_monoid_eqalgebra : monoid_eqalgebra.
  use make_eqalgebra.
  - exact (monoid_algebra M).
  - exact is_eqalgebra_monoid.
Defined.

End Make_Monoid_Eqalgebra.

End Eqspec.