C D (F G : Functor C D) (T' : F = G) x : (Category.Morphisms.idtoiso (_ -> _) T' : morphism _ _ _) x = Category.Morphisms.idtoiso _ (ap10 (ap object_of T') x). Proof. destruct T'. reflexivity. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import NaturalTransformation.Composition.Core. Require Import Functor.Composition.Core. Require Import Category.Morphisms. Require Import FunctorCategory.Core. Require Import NaturalTransformation.Paths. Require Import Basics.Tactics.