proposition: Lemma pseudofunctor_of_functor__left_identity_of {x0 x : PreCategory} {x2 : Functor x x} {x3 : x2 = 1%functor} {x4 x5 : Functor x0 x} {x6 : x4 = x5} {x7 : x4 = (x2 o x5)%functor} (H0' : P x0) (H' : P x) : ((Category.Morphisms.idtoiso (x -> x) x3 : morphism _ _ _) oR x5 o (Category.Morphisms.idtoiso (x0 -> x) x7 : morphism _ _ _))%natural_transformation = ((NaturalTransformation.Composition.Laws.left_identity_natural_transformation_2 x5) o (Category.Morphisms.idtoiso (x0 -> x) x6 : morphism _ _ _))%natural_transformation.
proof: Proof. clear F. simpl; pseudofunctor_t. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws Functor.Identity Pseudofunctor.Core Cat.Core FunctorCategory.Core FunctorCategory.Morphisms NaturalTransformation.Isomorphisms Category.Morphisms NaturalTransformation.Paths Basics.PathGroupoids Basics.Trunc