Definition is_pointwise_z_iso_if_is_disp_functor_cat_z_iso (x y : FunctorsC'C) (f : z_iso x y) (xx : disp_functor_cat x) (yy : disp_functor_cat y) (FF : xx -->[ f ] yy) (H : is_z_iso_disp f FF) : forall x' (xx' : D' x') , is_z_iso_disp (pointwise_z_iso_from_nat_z_iso f _ ) (pr1 FF _ xx' ). Proof. intros x' xx'. use tpair. - set (X:= pr1 H). simpl in X. apply (transportb _ (pointwise_inv_is_inv_on_z_iso f _ ) (X x' xx')). - simpl. repeat split. + etrans. apply mor_disp_transportf_postwhisker. apply pathsinv0. apply transportf_comp_lemma. assert (XR:= pr1 (pr2 H)). assert (XRT := (maponpaths pr1 XR)). assert (XRT' := toforallpaths _ _ _ (toforallpaths _ _ _ XRT x')). apply pathsinv0. etrans. apply XRT'. clear XRT' XRT XR. assert (XR := @disp_nat_trans_transportf C' C D' D). specialize (XR _ _ _ _ (! z_iso_after_z_iso_inv f)). etrans. apply XR. apply maponpaths_2, homset_property. + etrans. apply mor_disp_transportf_prewhisker. apply pathsinv0. apply transportf_comp_lemma. assert (XR:= inv_mor_after_z_iso_disp H). assert (XRT := (maponpaths pr1 XR)). assert (XRT' := toforallpaths _ _ _ (toforallpaths _ _ _ XRT x')). apply pathsinv0. etrans. apply XRT'. clear XRT' XRT XR. assert (XR := @disp_nat_trans_transportf C' C D' D). specialize (XR _ _ _ _ (! z_iso_inv_after_z_iso f)). etrans. apply XR. apply maponpaths_2, homset_property. 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.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.