Proposition isaprop_hfiber_ff_disp {C₁ C₂ : category} {F : C₁ ⟶ C₂} {D₁ : disp_cat C₁} {D₂ : disp_cat C₂} (HD₁ : is_univalent_disp D₁) (HD₂ : is_univalent_disp D₂) {FF : disp_functor F D₁ D₂} (HFF : disp_functor_ff FF) (x : C₁) (yy : D₂(F x)) : isaprop (hfiber (FF x) yy). Proof. use invproofirrelevance. intros φ₁ φ₂. induction φ₁ as [ ww₁ ι₁ ]. induction φ₂ as [ ww₂ ι₂ ]. enough (∑ (p : ww₁ = ww₂), maponpaths (FF x) p = ι₁ @ !ι₂) as p. { use total2_paths_f. - exact (pr1 p). - rewrite transportf_paths_FlFr. cbn. rewrite maponpaths_for_constant_function. rewrite pathscomp0rid. rewrite (pr2 p). rewrite pathscomp_inv. rewrite pathsinv0inv0. rewrite <- path_assoc. rewrite pathsinv0l. rewrite pathscomp0rid. apply idpath. } enough (∑ (p : z_iso_disp (identity_z_iso _) ww₁ ww₂), ♯FF p = transportb (λ z, _ -->[ z ] _) (functor_id F _) (pr1 (idtoiso_disp (idpath _) (ι₁ @ !ι₂)))) as p. { refine (isotoid_disp HD₁ (idpath _) (pr1 p) ,, _). use (invmaponpathsincl _ (isinclweq _ _ _ (HD₂ _ _ (idpath _) _ _))). cbn -[idtoiso_disp]. use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ]. refine (pr1_idtoiso_disp_functor _ _ @ _). rewrite idtoiso_isotoid_disp. use transportf_transpose_left. exact (pr2 p). } pose (disp_functor_ff_inv _ HFF (transportb (λ z, _ -->[ z ] _) (functor_id F _) (pr1 (idtoiso_disp (idpath _) (ι₁ @ !ι₂))))) as ff. simple refine ((ff ,, _) ,, _). - apply FFinv_on_z_iso_is_z_iso. use is_z_iso_disp_transportb_fun_eq. apply idtoiso_disp. - apply FF_disp_functor_ff_inv. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq.