:: deftheorem defines comp-reversing FUNCTOR0:def 24 :
for C1 being non empty transitive AltCatStr
for C2 being non empty reflexive AltCatStr
for F being feasible Contravariant FunctorStr over C1,C2 holds
( F is comp-reversing iff for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . f) * (F . g) );