:: deftheorem Def9 defines Contravariant_Functor OPPCAT_1:def 9 :
for C, D being Category
for b₃ being Function of the carrier' of C, the carrier' of D holds
( b₃ is Contravariant_Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b₃ . (id c) = id d ) & ( for f being Morphism of C holds
( b₃ . (id (dom f)) = id (cod (b₃ . f)) & b₃ . (id (cod f)) = id (dom (b₃ . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b₃ . (g (*) f) = (b₃ . f) (*) (b₃ . g) ) ) );