:: deftheorem defines Functor ISOCAT_1:def 1 :
for C, D being Category
for b₃ being M3( bool [: the carrier' of b₁, the carrier' of b₂:]) holds
( b₃ is Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b₃ . (id c) = id d ) & ( for f being Morphism of C holds
( b₃ . (id (dom f)) = id (dom (b₃ . f)) & b₃ . (id (cod f)) = id (cod (b₃ . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
b₃ . (g (*) f) = (b₃ . g) (*) (b₃ . f) ) ) );