Implicit Arguments On.
Module Type Cat_Sig___.
Variable Morph : Obj->Obj->Type.
Variable morph_comp : (x,y,z:Obj; g:(Morph y z); f:(Morph x y))
(Morph x z).
Variable morph_id : (x:Obj) (Morph x x).
Axiom 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).
Axiom morph_id_sx : (A,B:Obj; F:(Morph A B))
(morph_comp (morph_id B) F)==F.
Axiom morph_id_dx : (A,B:Obj; F:(Morph A B))
(morph_comp F (morph_id A))==F.
End Cat_Sig___.