Category of T-algebra in ConCaT

Alg.v

Require Import ConCaT.CATEGORY_THEORY.FUNCTOR.Functor.


Section alg_def.

Variables (A : Category) (T : Functor A A).

Structure Alg_ob : Type := {Ob_alg_ob : A; Mor_alg_ob  : T Ob_alg_ob --> Ob_alg_ob}.

 Section alg_arrow_def.
 
 Variable axf byg : Alg_ob.

 Definition Alg_law (h : Ob_alg_ob axf --> Ob_alg_ob byg) :=
   Mor_alg_ob axf o h =_S (FMor T h) o Mor_alg_ob byg.

 Structure > Alg_arrow : Type :=
   {Mor_alg_arrow : Ob_alg_ob axf --> Ob_alg_ob byg;
    Prf_alg_law :> Alg_law Mor_alg_arrow}.

 (*** rewrite ***)

Definition Equal_alg_arrow (h h' : Alg_arrow) :=
  Mor_alg_arrow h =_S Mor_alg_arrow h'.

Lemma Equal_alg_arrow_equiv : Equivalence Equal_alg_arrow.
Proof.
apply Build_Equivalence; unfold Equal_alg_arrow in |- *.
unfold Reflexive in |- *; intro f.
apply Refl.
apply Build_Partial_equivalence.
unfold Transitive in |- *; intros f g h H1 H2.
apply Trans with (Mor_alg_arrow g); assumption.
unfold Symmetric in |- *; intros f g H.
apply Sym; assumption.
Qed.

Canonical Structure Alg_arrow_setoid : Setoid := Equal_alg_arrow_equiv.

End alg_arrow_def.

(* composision of two arrows in alg *)

Section comp_alg_def.

Variables (axf byg czh : Alg_ob) (f : Alg_arrow axf byg)
  (g : Alg_arrow byg czh).

Check Mor_alg_arrow.
(*
Mor_alg_arrow
     : forall axf byg : Alg_ob,
       Alg_arrow axf byg -> (Ob_alg_ob axf --> Ob_alg_ob byg)
*)


Definition Comp_alg_mor := (Mor_alg_arrow axf byg f) o Mor_alg_arrow byg czh g.

Lemma Comp_alg_law : Alg_law axf czh Comp_alg_mor.
Proof.
unfold Alg_law, Comp_alg_mor in |- *.
(* *) apply Trans with 
   ((FMor T (Mor_alg_arrow axf byg f) o FMor T (Mor_alg_arrow byg czh g)) o 
   Mor_alg_ob czh).
apply Trans with
   (FMor T (a:=Ob_alg_ob axf) (b:=Ob_alg_ob byg) (Mor_alg_arrow axf byg f)
    o Mor_alg_ob byg
   o Mor_alg_arrow byg czh g).
apply Trans with
  ((Mor_alg_ob axf o Mor_alg_arrow axf byg f) o Mor_alg_arrow byg czh g).
apply Prf_ass.
apply Trans with
   ((FMor T (a:=Ob_alg_ob axf) (b:=Ob_alg_ob byg) (Mor_alg_arrow axf byg f)
   o Mor_alg_ob byg) o Mor_alg_arrow byg czh g).
apply Comp_r.
apply (Prf_alg_law axf byg f).
apply Ass1.
apply Trans with
   (FMor T (a:=Ob_alg_ob axf) (b:=Ob_alg_ob byg) (Mor_alg_arrow axf byg f)
    o FMor T (a:=Ob_alg_ob byg) (b:=Ob_alg_ob czh) (Mor_alg_arrow byg czh g)
   o Mor_alg_ob czh).
apply Comp_l.
apply (Prf_alg_law byg czh g).
apply Sym.
apply Ass1.

apply Comp_r.
apply Sym.
apply FComp.
Qed.

Check Build_Alg_arrow.

Canonical Structure Comp_alg_arrow := Build_Alg_arrow axf czh Comp_alg_mor Comp_alg_law.

End comp_alg_def.

(* composistion operator *)
Lemma Comp_alg_congl : Congl_law Comp_alg_arrow.
Proof.
unfold Congl_law in |- *; simpl in |- *.
intros a b c f1; elim f1; intros h e f2.
elim f2; intros h' e' f3; elim f3; intros h'' e''.
unfold Equal_alg_arrow in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
intro H; apply Comp_l; trivial.
Qed.

Lemma Comp_alg_congr : Congr_law Comp_alg_arrow.
Proof.
unfold Congr_law in |- *; simpl in |- *.
intros a b c f1; elim f1; intros h e f2.
elim f2; intros h' e' f3; elim f3; intros h'' e''.
unfold Equal_alg_arrow in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
intro H; apply Comp_r; trivial.
Qed.

Definition Comp_Alg := Build_Comp Comp_alg_congl Comp_alg_congr.

Lemma Assoc_Alg : Assoc_law Comp_Alg.
Proof.
unfold Assoc_law in |- *; intros a b c d f1; elim f1.
intros h1 e1 f2; elim f2; intros h2 e2 f3.
elim f3; intros h3 e3.
simpl in |- *; unfold Equal_alg_arrow in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
apply Ass.
Qed.

(* Id *)

Lemma Id_alg_law : forall axf : Alg_ob, Alg_law axf axf (Id (Ob_alg_ob axf)).
Proof.
intro axf; unfold Alg_law in |- *.
(* *) apply Trans with (Mor_alg_ob axf).
apply Sym.
apply Idr.
apply Trans with
(Id (FOb T (Ob_alg_ob axf)) o Mor_alg_ob axf).
apply Sym.
apply Idl.
apply Comp_r.
apply FId1.
Qed.

Canonical Structure Id_Alg (axf : Alg_ob) :=
  Build_Alg_arrow axf axf (Id (Ob_alg_ob axf)) (Id_alg_law axf).

Lemma Idl_Alg : Idl_law Comp_Alg Id_Alg.
Proof.
unfold Idl_law in |- *; intros a b f1; elim f1; intros h e.
simpl in |- *; unfold Equal_alg_arrow in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
apply Idl.
Qed.

Lemma Idr_Alg : Idr_law Comp_Alg Id_Alg.
Proof.
unfold Idr_law in |- *; intros a b f1; elim f1; intros h e.
simpl in |- *; unfold Equal_alg_arrow in |- *; simpl in |- *.
unfold Comp_alg_mor in |- *; simpl in |- *.
apply Idr.
Qed.

Canonical Structure Alg := Build_Category Assoc_Alg Idl_Alg Idr_Alg.

End alg_def.