Definition disp_functor_ff_reflects_isos {x y} {xx : D x} {yy : D y} {f : z_iso x y} (ff : xx -->[ f ] yy) (isiso: is_z_iso_disp (functor_on_z_iso F f) (♯ FF ff)) : is_z_iso_disp _ ff. Proof. set (FFffinv := inv_mor_disp_from_z_iso isiso). set (FFffinv':= transportf (λ f', _ -->[ _ ] _ ) (functor_on_inv_from_z_iso F f) FFffinv). cbn in FFffinv'. set (ffinv := FFinv FFffinv'). exists ffinv. split. - abstract (unfold ffinv, FFffinv'; clear ffinv FFffinv' ; apply (invmaponpathsweq (@FFweq _ _ _ _ _ )) ; cbn ; etrans ; [ apply (disp_functor_comp FF) | ] ; etrans ; [ apply maponpaths ; apply maponpaths_2 ; apply (homotweqinvweq (@FFweq _ _ _ _ _ )) | ] ; rewrite transportf_const ; unfold idfun ; unfold FFffinv ; clear FFffinv ; etrans ; [ apply maponpaths ; apply (z_iso_disp_after_inv_mor isiso) | ] ; etrans ; [ apply transport_f_f | ] ; apply pathsinv0 ; etrans ; [ apply (disp_functor_transportf _ FF) | ] ; etrans ; [ apply maponpaths ; apply disp_functor_id | ] ; etrans ; [ apply transport_f_f | ] ; apply maponpaths_2 ; apply homset_property). - abstract (unfold ffinv, FFffinv'; clear ffinv FFffinv' ; apply (invmaponpathsweq (@FFweq _ _ _ _ _ )) ; cbn ; etrans ; [ apply (disp_functor_comp FF) | ] ; etrans ; [ apply maponpaths ; apply maponpaths ; apply (homotweqinvweq (@FFweq _ _ _ _ _ )) | ] ; etrans ; [ apply maponpaths ; eapply maponpaths ; apply (eqtohomot (transportf_const _ _)) | ] ; etrans ; [ apply maponpaths ; unfold FFffinv ; apply (inv_mor_after_z_iso_disp isiso) | ] ; etrans ; [ apply transport_f_f | ] ; apply pathsinv0 ; etrans ; [ apply (disp_functor_transportf _ FF) | ] ; etrans ; [ apply maponpaths ; apply disp_functor_id | ] ; etrans ; [ apply transport_f_f | ] ; apply maponpaths_2 ; apply homset_property). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. 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.Fiber.