proposition: Lemma pseudofunctor_to_cat_left_identity_helper : forall {x1 x2 : C} {f : Category.Core.morphism C x2 x1} {p p0 : PreCategory} {f0 : Category.Core.morphism C x2 x1 -> Functor p0 p} {f1 : Functor p p} {x0 : Category.Core.morphism (_ -> _) (f0 (1 o f)) (f1 o f0 f)%functor} {x : Category.Core.morphism (_ -> _) f1 1%functor} {fst_hyp : 1 o f = f} (rewrite_hyp : forall x3 : p0, (idtoiso (p0 -> p) (ap f0 fst_hyp) : Category.Core.morphism _ _ _) x3 = 1 o (x ((f0 f) x3) o x0 x3)) {H0' : IsIsomorphism x0} {H1' : IsIsomorphism x} {x3 : p} {x4 : p0} {f' : Category.Core.morphism p ((f0 f) x4) x3}, exist (fun f2 : Category.Core.morphism C x2 x1 => Category.Core.morphism p ((f0 f2) x4) x3) (1 o f) (x x3 o (f1 _1 f' o x0 x4)) = (f; f').
proof: Proof. helper_t idtac. Qed.
imports: FunctorCategory.Morphisms Category.Core Functor.Core NaturalTransformation.Core Pseudofunctor.Core Pseudofunctor.RewriteLaws Category.Morphisms Cat.Morphisms Functor.Composition.Core Functor.Identity FunctorCategory.Core Basics Types HoTT.Tactics