# varieties.monoids

Require Import
abstract_algebra universal_algebra ua_homomorphisms workaround_tactics
categories.categories.
Require
categories.varieties categories.product forget_algebra forget_variety.

Inductive op := mult | one.

Definition sig: Signature := single_sorted_signature
(λ o, match o with one => O | mult => 2%nat end).

Section laws.
Global Instance: SemiGroupOp (Term0 sig nat tt) :=
fun x => App sig _ _ _ (App sig _ _ _ (Op sig nat mult) x).
Global Instance: MonoidUnit (Term0 sig nat tt) := Op sig nat one.

Local Notation x := (Var sig nat 0%nat tt).
Local Notation y := (Var sig nat 1%nat tt).
Local Notation z := (Var sig nat 2%nat tt).

Import notations.

Inductive Laws: EqEntailment sig Prop :=
| e_mult_assoc: Laws (x & (y & z) === (x & y) & z)
| e_mult_1_l: Laws (mon_unit & x === x)
| e_mult_1_r: Laws (x & mon_unit === x).
End laws.

Definition theory: EquationalTheory := Build_EquationalTheory sig Laws.
Definition Object := varieties.Object theory.

Local Hint Extern 3 => progress simpl : typeclass_instances.

Definition forget: Object setoids.Object :=
@product.project unit
(λ _, setoids.Object)
(λ _, _) _
(λ _, _) (λ _, _) (λ _, _) tt
forget_algebra.object theory forget_variety.forget theory.

Instance encode_operations A `{!SemiGroupOp A} `{!MonoidUnit A}: AlgebraOps sig (λ _, A) :=
λ o, match o with mult => (&) | one => mon_unit: A end.

Section decode_operations.
Context `{AlgebraOps theory A}.
Global Instance: MonoidUnit (A tt) := algebra_op one.
Global Instance: SemiGroupOp (A tt) := algebra_op mult.
End decode_operations.

Section encode_variety_and_ops.
Context A `{Monoid A}.

Global Instance encode_algebra_and_ops: Algebra sig _.

Global Instance encode_variety_and_ops: InVariety theory (λ _, A).

Definition object: Object := varieties.object theory (λ _, A).
End encode_variety_and_ops.

Lemma encode_algebra_only `{!AlgebraOps theory A} `{ u, Equiv (A u)} `{!Monoid (A tt)}: Algebra theory A .

Global Instance decode_variety_and_ops `{InVariety theory A}: Monoid (A tt).

Lemma encode_morphism_only
`{AlgebraOps theory A} `{ u, Equiv (A u)}
`{AlgebraOps theory B} `{ u, Equiv (B u)}
(f: u, A u B u) `{!Monoid_Morphism (f tt)}: HomoMorphism sig A B f.

Lemma encode_morphism_and_ops `{Monoid_Morphism A B f}:
@HomoMorphism sig (λ _, A) (λ _, B) _ _ ( _) ( _) (λ _, f).

Lemma decode_morphism_and_ops
`{InVariety theory x} `{InVariety theory y} `{!HomoMorphism theory x y f}:
Monoid_Morphism (f tt).

Section specialized.
Context (A B C: Type)
`{!MonoidUnit A} `{!SemiGroupOp A} `{!Equiv A}
`{!MonoidUnit B} `{!SemiGroupOp B} `{!Equiv B}
`{!MonoidUnit C} `{!SemiGroupOp C} `{!Equiv C}
(f: A B) (g: B C).

Global Instance id_morphism `{!Monoid A}: Monoid_Morphism id.

Global Instance compose_morphisms
`{!Monoid_Morphism f} `{!Monoid_Morphism g}: Monoid_Morphism (g f).

Global Instance: `{H: Monoid_Morphism A B f} `{!Inverse f},
Bijective f Monoid_Morphism (f⁻¹).
End specialized.