fact: Definition left_identity_natural_transformation_1 : NaturalTransformation (1 o F) F := Eval simpl in generalized_identity (1 o F) F idpath idpath.
imports: Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths