Library CatSem.CAT.cat_gen_monad

Require Export CatSem.CAT.monad_h_morphism_gen.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.

Section id.

Variable C : Cat.
Variable P : Monad C.

Obligation Tactic := cat.

Program Instance colax_Monad_Hom_id_s : colax_Monad_Hom_struct (P:=P)
  (F0 := Id C)
 (fun c => id _ ).

Definition colax_Monad_Hom_id := Build_colax_Monad_Hom colax_Monad_Hom_id_s.

End id.

Section comp.

Variable C : Cat.
Variable P : Monad C.
Variable D : Cat.
Variable Q : Monad D.
Variable E : Cat.
Variable R : Monad E.

Variable F : Functor C D.
Variable S : colax_Monad_Hom P Q F.
Variable G : Functor D E.
Variable T : colax_Monad_Hom Q R G.

Program Instance colax_Monad_Hom_comp_s : colax_Monad_Hom_struct (P:=P)
  (F0 := G O F)
 (fun c => #G(S c) ;; T (F c)).
Next Obligation.
Proof.
  repeat rewrite <-assoc.
  rewrite <- FComp.
  rewrite <- FComp.
  rewrite assoc.
  rerew (gen_monad_hom_kl (colax_Monad_Hom_struct := T)).
  rewrite <- assoc.
  rewrite <- FComp.
  rerew (gen_monad_hom_kl (colax_Monad_Hom_struct := S)).
  apply hom_refl.
Qed.
Next Obligation.
Proof.
  rewrite <- assoc.
  rewrite <- FComp.
  rewrite (gen_monad_hom_weta (colax_Monad_Hom_struct := S)).
  rewrite (gen_monad_hom_weta (colax_Monad_Hom_struct := T)).
  apply hom_refl.
Qed.

Definition colax_Monad_Hom_comp :=
    Build_colax_Monad_Hom colax_Monad_Hom_comp_s.

End comp.

Section eq.

Variable C : Cat.
Variable P : Monad C.
Variable D : Cat.
Variable Q : Monad D.

Record gen_Monad_Hom_type := {
 base_f : Functor C D ;
 gen_mon_hom :> colax_Monad_Hom P Q base_f
}.


End eq.