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