proposition: Lemma eta_idtoiso (F G : object (C -> D)) (T : F = G) : Category.Morphisms.idtoiso _ T = idtoiso T.
proof: Proof. case T. expand; f_ap. exact (center _). Qed.
imports: Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core Basics.Tactics