C D E (F : Functor D E) (G G' : Functor C D) (T : G = G') : whisker_l F (Category.Morphisms.idtoiso (_ -> _) T : morphism _ _ _) = (Category.Morphisms.idtoiso (_ -> _) (ap _ T) : morphism _ _ _). Proof. path_natural_transformation; path_induction; simpl; auto with functor. 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.