:: deftheorem Def20 defines id-preserving FUNCTOR0:def 20 :
for C1, C2 being non empty with_units AltCatStr
for F being FunctorStr over C1,C2 holds
( F is id-preserving iff for o being Object of C1 holds (Morph-Map (F,o,o)) . (idm o) = idm (F . o) );