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