:: deftheorem Def12 defines Covariant FUNCTOR0:def 12 :
for C1, C2 being 1-sorted
for IT being BimapStr over C1,C2 holds
( IT is Covariant iff the ObjectMap of IT is Covariant );