:: deftheorem defines contravariant CAT_6:def 26 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is contravariant iff ( F is identity-preserving & F is antimultiplicative ) );