:: deftheorem defines coreflexive FUNCTOR0:def 9 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is coreflexive iff id the carrier of B c= the ObjectMap of F .: (id the carrier of A) );