C D F G H I (V : @NaturalTransformation C D F G) (U : @NaturalTransformation C D G H) (T : @NaturalTransformation C D H I) : (T o U) o V = T o (U o V). Proof. path_natural_transformation. apply . Qed.
Require Import Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths.