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

Inductive op := mult.

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

Section laws.
  Global Instance: SemiGroupOp (Term0 sig nat tt) :=
    λ x, App sig _ _ _ (App sig _ _ _ (Op sig nat mult) x).

  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).
End laws.

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

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

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

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

Section encode_variety_and_ops.
  Context A `{SemiGroup 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)} `{!SemiGroup (A tt)}: Algebra theory A .

Global Instance decode_variety_and_ops `{InVariety theory A}: SemiGroup (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) `{!SemiGroup_Morphism (f tt)}: HomoMorphism sig A B f.

Lemma encode_morphism_and_ops `{SemiGroup_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}:
    SemiGroup_Morphism (f tt).

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

  Global Instance id_morphism `{!SemiGroup A}: SemiGroup_Morphism id.

  Global Instance compose_morphisms `{!SemiGroup A, !SemiGroup B, !SemiGroup C}
    `{!SemiGroup_Morphism f} `{!SemiGroup_Morphism g}: SemiGroup_Morphism (g f).

  Global Instance: `{H: SemiGroup_Morphism A B f} `{!Inverse f},
    Bijective f SemiGroup_Morphism (inverse f).
End specialized.