proposition: Lemma pseudofunctor_to_cat_right_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 p0 p0} {x0 : Category.Core.morphism (_ -> _) (f0 (f o 1)) (f0 f o f1)%functor} {H0' : IsIsomorphism x0} {x : Category.Core.morphism (_ -> _) f1 1%functor} {H1' : IsIsomorphism x} {fst_hyp : f o 1 = f} (rew_hyp : forall x3 : p0, (idtoiso (p0 -> p) (ap f0 fst_hyp) : Category.Core.morphism _ _ _) x3 = 1 o ((f0 f) _1 (x x3) o x0 x3)) {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) (f o 1) (f' o ((f0 f) _1 (x x4) 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