proposition: Lemma composition_of_whisker_l E (I : Functor D E) : I oL (T o T') = (I oL T) o (I oL T').
proof: Proof. path_natural_transformation; apply composition_of. Qed.
imports: Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths