:: deftheorem Def26 defines covariant FUNCTOR0:def 26 :
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 covariant iff ( F is Covariant & F is comp-preserving ) );