Definition fiber_functor_ess_split_surj {C C' : category} {D} {D'} {F : functor C C'} (FF : disp_functor F D D') (H : disp_functor_ff FF) {X : disp_functor_ess_split_surj FF} {Y : is_op_isofibration D} (x : C) : ∏ yy : D'[{F x}], ∑ xx : D[{x}], z_iso (fiber_functor FF _ xx) yy. Proof. intro yy. set (XR := X _ yy). destruct XR as [c'' [i [xx' ii]]]. set (YY := Y _ _ i xx'). destruct YY as [ dd pe ]. use tpair. - apply dd. - set (XR := disp_functor_on_z_iso_disp FF pe). set (XR' := z_iso_inv_from_z_iso_disp XR). apply (invweq (z_iso_disp_z_iso_fiber _ _ _ _)). set (XRt := z_iso_disp_comp XR' ii). transparent assert (XH : (z_iso_comp (z_iso_inv_from_z_iso (functor_on_z_iso F i)) (functor_on_z_iso F i) = identity_z_iso _ )). { apply z_iso_eq. cbn. etrans. { apply pathsinv0, functor_comp. } apply functor_id_id. apply z_iso_after_z_iso_inv. } set (XRT := transportf (λ r, z_iso_disp r (FF x dd) yy ) XH). apply XRT. assumption. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite. Section IsoCleavingFromOpcleaving. End IsoCleavingFromOpcleaving.