proposition: Lemma identity_left_identity (x y : PreCategory) (f : Functor x y) : 1 oR f o 1 = (left_identity_natural_transformation_2 f) o @morphism_isomorphic _ _ _ (idtoiso (x -> y) (ap idmap (Functor.Composition.Laws.left_identity f))).
proof: Proof. t. Defined.
imports: FunctorCategory.Morphisms Category.Core Functor.Core NaturalTransformation.Isomorphisms NaturalTransformation.Paths Cat.Core Pseudofunctor.Core PathGroupoids