Library UniMath.Algebra.Universal.Examples.Group
Example on groups.
Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021Require Import UniMath.MoreFoundations.Notations.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.MoreLists.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.Universal.EqAlgebras.
Local Open Scope stn.
Local Open Scope eq.
Group structure without equations.
Definition group_signature := make_signature_simple_single_sorted [2; 0; 1].
Definition group_sort : sorts group_signature := tt.
Definition group_mul_op: names group_signature := ●0.
Definition group_id_op: names group_signature := ●1.
Definition group_inv_op: names group_signature := ●2.
Algebra of groups.
Module Algebra.
Definition group_algebra {G: gr}
:= make_algebra_simple_single_sorted' group_signature G [( op ; unel G; grinv G )].
Definition group_mul := build_gterm' group_mul_op.
Definition group_id := build_gterm' group_id_op.
Definition group_inv := build_gterm' group_inv_op.
End Algebra.
Module Eqspec.
Equational specification and the free algebra of open terms.
Definition group_varspec : varspec group_signature := make_varspec group_signature natset (λ _, group_sort).
Definition G := term group_signature group_varspec group_sort.
Definition group_mul: G → G → G := build_term' group_mul_op.
Definition group_id: G := build_term' group_id_op.
Definition group_inv: G → G := build_term' group_inv_op.
Definition x : G := varterm (0: group_varspec).
Definition y : G := varterm (1: group_varspec).
Definition z : G := varterm (2: group_varspec).
Definition group_mul_assoc := group_mul (group_mul x y) z == group_mul x (group_mul y z).
Definition group_mul_lid := group_mul group_id x == x.
Definition group_mul_rid := group_mul group_id x == x.
Definition group_axioms : eqsystem group_signature group_varspec :=
⟦ 3 ⟧,, three_rec group_mul_assoc group_mul_lid group_mul_rid.
Definition group_eqspec : eqspec.
Proof.
use tpair. { exact group_signature. }
use tpair. { exact group_varspec. }
exact group_axioms.
Defined.
Definition group_eqalgebra := eqalgebra group_eqspec.
End Eqspec.