:: deftheorem Def25 defines covariant CAT_6:def 25 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is covariant iff ( F is identity-preserving & F is multiplicative ) );