If (μFG, in) is initial FG-algebra, then (GμFG, Gin) is initial GF-algebra.

ALG2.v

(*
 Let F: C→D and G: D→C be functors.
 If (μFG, in) is initial FG-algebra, then (GμFG, Gin) is initial GF-algebra.
 Based on https://gist.github.com/955007
*)

Require Export Functor.

Set Implicit Arguments.
Unset Strict Implicit.

Section alg_def.

Variable (C : Category).
Variable (F : Functor C C).

Structure Alg_ob : Type :=
  { Ob_alg_ob :> C
  ; Mor_alg_ob :> F Ob_alg_ob --> Ob_alg_ob
  }.

Definition Alg_law (a : Alg_ob) (b : Alg_ob) (h : a --> b) :=
  a o h =_S FMor F h o b .

Structure Alg_mor (a : Alg_ob) (b : Alg_ob) : Type :=
  { Mor_alg_mor :> a --> b
  ; Prf_Alg_law :> Alg_law Mor_alg_mor
  }.

Section equal_alg_mor.

Variables a b : Alg_ob.

Definition Equal_Alg_mor (f g : Alg_mor a b) :=
  Mor_alg_mor f =_S Mor_alg_mor g 
  .

Lemma Equal_Alg_mor_equiv : Equivalence Equal_Alg_mor.
Proof.
unfold Equal_Alg_mor.
apply Build_Equivalence.
red.
intro.
apply Refl.
apply Build_Partial_equivalence.
red.
intros x y z.
apply Trans.
red.
intros x y.
apply Sym.
Qed.

Canonical Structure Alg_mor_setoid : Setoid := Equal_Alg_mor_equiv.

End equal_alg_mor.

Section comp_alg_mor.

Variables (a b c : Alg_ob) (f : Alg_mor a b) (g : Alg_mor b c).

Lemma Comp_Alg_mor_law : Alg_law (f o g).
Proof.
red.
apply Trans with ((a o f) o g).
apply Ass.
apply Trans with ((FMor F f o b) o g).
apply Comp_r.
apply Prf_Alg_law.
apply Trans with (FMor F f o (b o g)).
apply Ass1.
apply Trans with ((FMor F f o FMor F g o c)).
apply Comp_l.
apply Prf_Alg_law.
apply Trans with ((FMor F f o FMor F g) o c).
apply Ass.
apply Comp_r.
apply FComp1.
Qed.

Definition Comp_Alg_mor: Alg_mor a c :=
  Build_Alg_mor Comp_Alg_mor_law.

End comp_alg_mor.

Lemma Comp_Alg_mor_congl : Congl_law Comp_Alg_mor.
Proof.
red.
intros a b c f g h eq.
simpl.
unfold Comp_Alg_mor.
unfold Equal_Alg_mor.
red.
apply Comp_l.
apply eq.
Qed.

Lemma Comp_Alg_mor_congr : Congr_law Comp_Alg_mor.
Proof.
red.
intros a b c f g h eq.
simpl.
unfold Comp_Alg_mor.
unfold Equal_Alg_mor.
red.
apply Comp_r.
apply eq.
Qed.

Definition Comp_Alg := Build_Comp Comp_Alg_mor_congl Comp_Alg_mor_congr.

Lemma Assoc_Alg : Assoc_law Comp_Alg.
Proof.
unfold Assoc_law.
intros a b c d f g h.
unfold Cat_comp.
unfold Comp_Alg.
simpl.
unfold Alg_mor_setoid, Comp_Alg_mor.
unfold Equal_Alg_mor.
simpl.
apply Ass.
Qed.

Section id_alg_mor.
Variables (a : Alg_ob).

Lemma Id_Alg_mor_law : Alg_law (Id a).
Proof.
red.
apply Trans with (Mor_alg_ob a).
apply Idr1.
apply Trans with (Id (F a) o a).
apply Idl1.
apply Comp_r.
apply FId1.
Qed.

Definition Id_Alg : Alg_mor a a := Build_Alg_mor Id_Alg_mor_law.

End id_alg_mor.

Lemma Idl_Alg : Idl_law Comp_Alg Id_Alg.
Proof.
red.
intros a b f.
unfold Cat_comp.
unfold Comp_Alg.
simpl.
unfold Equal_Alg_mor.
simpl.
apply Idl.
Qed.

Lemma Idr_Alg : Idr_law Comp_Alg Id_Alg.
Proof.
red.
intros a b f.
unfold Cat_comp.
unfold Comp_Alg.
simpl.
unfold Equal_Alg_mor.
simpl.
apply Idr.
Qed.

Canonical Structure Alg := Build_Category Assoc_Alg Idl_Alg Idr_Alg.

End alg_def.


Require Export CatProperty.

Section initial_algebra.

Variable (C : Category).
Variable (F : Functor C C).
Variable (initial : Initial (Alg F)).

Let muF := Initial_ob initial.
Let inF := Mor_alg_ob muF.
Let fold := MorI initial.
Let FmuF := Build_Alg_ob (FMor F muF).

Lemma inF_Alg_law : Alg_law (a:=FmuF) (b:=muF) inF.
Proof.
apply Refl.
Qed.

Let inF' := Build_Alg_mor inF_Alg_law.
Definition unInF' := fold (Build_Alg_ob (FMor F inF)).
Definition unInF := Mor_alg_mor unInF'.

Lemma lem1 : RIso_law inF' unInF'.
unfold RIso_law.
apply (UniqueI (unInF' o inF') (Id muF)).
Qed.

Lemma lem2 : RIso_law unInF inF.
unfold RIso_law.
apply Trans with (FMor F unInF o FMor F inF).
apply (Prf_Alg_law unInF').
apply Trans with (FMor F (unInF o inF)).
apply FComp1.
apply Trans with (FMor F (Id (Ob_alg_ob muF))).
apply FPres.
apply lem1.
apply FId.
Qed.

Lemma LambekLemma : AreIsos inF unInF.
unfold AreIsos.
split.
apply lem1.
apply lem2.
Qed.

End initial_algebra.

Section cata_fusion.
Variable (C : Category).
Variable (F : Functor C C).
Variable (initial : Initial (Alg F)).
Let muF := Initial_ob initial.
Let inF := Mor_alg_ob muF.
Let fold := MorI initial.
Let FmuF := Build_Alg_ob (FMor F muF).

Variable (phi psi : Alg F).
Variable h : phi --> psi.

Lemma cataFusion : fold phi o h =_S fold psi.
apply (UniqueI (fold phi o h) (fold psi)).
Qed.

End cata_fusion.

Section FLift_def.
Variable (C D : Category).
Variable (F : Functor C D).
Variable (G : Functor D C).
Let FG : Functor D D := G o_F F.
Let GF : Functor C C := F o_F G.

Definition FLift_FOb (phi : Alg GF) : Alg FG
:= Build_Alg_ob (FMor F (Mor_alg_ob phi) : FG (F (Ob_alg_ob phi)) --> F (Ob_alg_ob phi)).

Section FLift_FMap_def.
Variable (phi psi : Alg GF).
Let X : C := Ob_alg_ob phi.
Let Y : C := Ob_alg_ob psi.
Let FX : D := F X.
Let FY : D := F Y.
Let Fphi : Alg FG := FLift_FOb phi.
Let Fpsi : Alg FG := FLift_FOb psi.

Section FLift_FMap_map_def.
Variable h : phi --> psi.

Definition FLift_Fmap_map_map : F X --> F Y
:= FMor F (Mor_alg_mor h).

Lemma FLift_Fmap_map_law : Alg_law (a:=Fphi) (b:=Fpsi) FLift_Fmap_map_map.
unfold Alg_law.
unfold FLift_Fmap_map_map.
apply Trans with (FMor F (Mor_alg_ob phi) o FMor F (Mor_alg_mor h)).
apply Refl.
apply Trans with (FMor F (Mor_alg_ob phi o Mor_alg_mor h)).
apply FComp1.
apply Trans with (FMor F (FMor GF (Mor_alg_mor h) o Mor_alg_ob psi)).
apply FPres.
apply (Prf_Alg_law h).
apply Trans with (FMor F (FMor GF (Mor_alg_mor h)) o FMor F (Mor_alg_ob psi)).
apply FComp.
apply Refl.
Qed.

Definition FLift_FMap_map : Fphi --> Fpsi
:= Build_Alg_mor FLift_Fmap_map_law.

End FLift_FMap_map_def.

Lemma FLift_FMap_law : Map_law FLift_FMap_map.
unfold Map_law.
intros.
apply (FPres F (a:=Ob_alg_ob phi) (b:=Ob_alg_ob psi) H).
Qed.

Definition FLift_FMap : Map (phi --> psi) (Fphi --> Fpsi)
:= Build_Map FLift_FMap_law.

End FLift_FMap_def.

Lemma FLift_Fcomp_law : Fcomp_law FLift_FMap.
unfold Fcomp_law.
intros.
apply (FComp F f g).
Qed.

Lemma FLift_Fid_law : Fid_law FLift_FMap.
unfold Fid_law.
intros.
apply (FId F a).
Qed.

Definition FLift : Functor (Alg GF) (Alg FG)
:= Build_Functor FLift_Fcomp_law FLift_Fid_law.

End FLift_def.

Section theorem.

Variable (C D : Category).
Variable (F : Functor C D).
Variable (G : Functor D C).
Let FG : Functor D D := G o_F F.
Let GF : Functor C C := F o_F G.

Let F2 : Functor (Alg GF) (Alg FG) := FLift F G.
Let G2 : Functor (Alg FG) (Alg GF) := FLift G F.
Let FG2 : Functor (Alg FG) (Alg FG) := G2 o_F F2.
Let GF2 : Functor (Alg GF) (Alg GF) := F2 o_F G2.

Variable (initialFG : Initial (Alg FG)).

Let muFG : Alg FG := Initial_ob initialFG.
Let inFG := Mor_alg_ob muFG.
Let foldFG := MorI initialFG.
Let GmuFG : Alg GF := G2 muFG.
Let FGmuFG : Alg FG := F2 GmuFG.

Section foldGF_def.

Variable phi : Alg GF.
Let X : C := Ob_alg_ob phi.
Let Fphi : Alg FG := F2 phi.
Let GFphi : Alg GF := G2 Fphi.

Let h1 : GmuFG --> GFphi := FMor G2 (foldFG Fphi).

Lemma h2_Alg_law : Alg_law (a:=GFphi) (b:=phi) (Mor_alg_ob phi).
apply Refl.
Qed.

Let h2 : GFphi --> phi := Build_Alg_mor h2_Alg_law.

Definition foldGF : GmuFG --> phi := h1 o h2.

Section uniqueness.

Variable f : GmuFG --> phi.
Let Ff : FGmuFG --> Fphi := FMor F2 f.

Lemma lemma1 : FMor FG inFG o Ff =_S FMor FG Ff o Fphi.
apply Trans with (FMor F (FMor G inFG) o FMor F f).
apply Refl.
apply Trans with (FMor F (FMor G inFG o f)).
apply FComp1.
apply Trans with (FMor F (FMor GF f o phi)).
apply FPres.
apply (Prf_Alg_law f).
apply FComp.
Qed.

Let unInFG : Ob_alg_ob muFG --> Ob_alg_ob FGmuFG := unInF initialFG.

Lemma uniqueness' : Mor_alg_mor f =_S Mor_alg_mor foldGF.
apply Trans with (Id (Ob_alg_ob GmuFG) o Mor_alg_mor f).
apply Idl1.

apply Trans with (FMor G (Id (Ob_alg_ob muFG)) o Mor_alg_mor f).
apply Comp_r.
apply FId1.

apply Trans with (FMor G (unInFG o inFG) o Mor_alg_mor f).
apply Comp_r.
apply FPres.
apply Sym.
destruct (LambekLemma (C:=D) (F:=FG) initialFG).
apply H.

apply Trans with ((FMor G unInFG o FMor G inFG) o f).
apply Comp_r.
apply FComp.

apply Trans with
(FMor G unInFG o ((FMor G inFG) o Mor_alg_mor f)).
apply Ass1.

apply Trans with
(FMor G unInFG o (FMor GF (Mor_alg_mor f)) o phi).
apply Comp_l.
apply (Prf_Alg_law f).

apply Trans with
((FMor G unInFG o FMor GF (Mor_alg_mor f)) o phi).
apply Ass.

apply Trans with
(FMor G (unInFG o FMor F (Mor_alg_mor f)) o phi).
apply Comp_r.
apply Trans with
(FMor G unInFG o FMor G (FMor F (Mor_alg_mor f))).
apply Refl.
apply FComp1.

apply Trans with
(FMor G (Mor_alg_mor (foldFG FGmuFG) o FMor F (Mor_alg_mor f)) o phi).
apply Refl.

apply Trans with
(FMor G (foldFG Fphi) o phi).
apply Comp_r.
apply FPres.
apply (cataFusion initialFG Ff).

apply Refl.
Qed.

Lemma uniqueness : f =_S foldGF.
apply uniqueness'.
Qed.

End uniqueness.

End foldGF_def.

Theorem GmuFG_IsInitial : IsInitial foldGF.
unfold IsInitial.
intros.
apply uniqueness.
Qed.

End theorem.