:: deftheorem Def3 defines idt FUNCTOR2:def 3 :
for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for b₄ being transformation of F,F holds
( b₄ = idt F iff for a being Object of A holds b₄ . a = idm (F . a) );