:: deftheorem Def25 defines Functor FUNCTOR0:def 25 :
for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for b₃ being FunctorStr over C1,C2 holds
( b₃ is Functor of C1,C2 iff ( b₃ is feasible & b₃ is id-preserving & ( ( b₃ is Covariant & b₃ is comp-preserving ) or ( b₃ is Contravariant & b₃ is comp-reversing ) ) ) );