(G' oL T) o (T' oR F) = (T' oR F') o (G oL T). Proof. path_natural_transformation; simpl. symmetry. apply NaturalTransformation.Core.commutes. Qed.
Require Import Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths.