proposition: Lemma left_identity (F F' : Functor C D) (T : NaturalTransformation F F') : 1 o T = T.
proof: Proof. path_natural_transformation; auto with morphism. Qed.
imports: Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths