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. helper_t idtac. Qed.
Require Import FunctorCategory.Morphisms. Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Pseudofunctor.Core Pseudofunctor.RewriteLaws. Require Import Category.Morphisms Cat.Morphisms. Require Import Functor.Composition.Core. Require Import Functor.Identity. Require Import FunctorCategory.Core. Require Import Basics Types HoTT.Tactics.