:: deftheorem Def27 defines contravariant FUNCTOR0:def 27 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 holds
( F is contravariant iff ( F is Contravariant & F is comp-reversing ) );