for A, B being category
for F1 being covariant Functor of A,B holds (idt F1) " = idt F1