:: deftheorem defines IdMap ISOCAT_1:def 12 :
for C being Category
for b₂ being Function of the carrier of C, the carrier' of C holds
( b₂ = IdMap C iff for o being Object of C holds b₂ . o = id o );