:: deftheorem defines monomorphism CAT_7:def 18 :
for C, D being category
for F being Functor of C,D holds
( F is monomorphism iff ( F is covariant & ( for B being category
for G1, G2 being Functor of B,C st G1 is covariant & G2 is covariant & F (*) G1 = F (*) G2 holds
G1 = G2 ) ) );