proposition: Lemma composition_of_whisker_r B (I : Functor B C) : (T o T') oR I = (T oR I) o (T' oR I).
proof: Proof. path_natural_transformation; apply idpath. Qed.
imports: Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths