for A being discrete Category
for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F