for C, D being with_identities CategoryStr st not C is empty & D is empty holds
for F being Functor of C,D holds
( not F is covariant & not F is contravariant ) by Th29;