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