proposition: Theorem left_identity_isomorphism : left_identity_natural_transformation_1 o left_identity_natural_transformation_2 = 1 /\ left_identity_natural_transformation_2 o left_identity_natural_transformation_1 = 1.
proof: Proof. nt_id_t. Qed.
imports: Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths