NaturalTransformation F (1 o F) := Eval simpl in generalized_identity F (1 o F) idpath idpath.
Require Import Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths.