Require Export nt_.
Require make_small_cat_.
Implicit Arguments On.
Category of functors. |
Module Fct_Cat_ [AA,BB:A_Cat_] <: Cat_Sig_.
Export Misc_.
Export NT_.
Definition Obj : Type := (Functor AA.A BB.A).
Definition Morph [A,B:Obj] : Type := (NT A B).
Definition morph_comp : (x,y,z:Obj; g:(Morph y z); f:(Morph x y))
(Morph x z) := (!nt_comp AA.A BB.A).
Definition morph_id : (x:Obj) (Morph x x) := (!nt_id AA.A BB.A).
Definition morph_comp_assoc : (A,B,C,D:Obj)
(H:(Morph C D); G:(Morph B C); F:(Morph A B))
(morph_comp H (morph_comp G F))==(morph_comp (morph_comp H G) F).
Proof.
Intros; Unfold Morph Obj morph_comp; Simpl.
Apply (!nt_comp_assoc AA.A BB.A).
Qed.
Definition morph_id_sx : (A,B:Obj; F:(Morph A B))
(morph_comp (morph_id B) F)==F.
Proof.
Intros; Unfold Morph Obj morph_comp morph_id; Simpl.
Apply (!nt_sx_id AA.A BB.A).
Qed.
Definition morph_id_dx : (A,B:Obj; F:(Morph A B))
(morph_comp F (morph_id A))==F.
Proof.
Intros; Unfold Morph Obj morph_comp morph_id; Simpl.
Apply (!nt_dx_id AA.A BB.A).
Qed.
End Fct_Cat_.
| Test |
Parameter my_cat_A, my_cat_B : Cat_.Cat. Module my_AA : A_Cat_. Definition A := my_cat_A. End my_AA. Module my_BB : A_Cat_. Definition A := my_cat_A. End my_BB. Module my_Fct_Cat := (Fct_Cat_ my_AA my_BB). Module my_small_fct_cat := (Make_Small_Cat_ my_Fct_Cat).
|