Definition FFinv_over_id_on_z_iso_is_z_iso {x y} {xx : D' x} {yy : D' y} {f : z_iso x y} (ff : FF _ xx -->[ f ] FF _ yy) (Hff: is_z_iso_disp f ff) : is_z_iso_disp _ (FFinv ff). Proof. apply disp_functor_id_ff_reflects_isos. use (transportf _ _ Hff). apply @pathsinv0. use homotweqinvweq. Qed. Local Definition GG_data : disp_functor_data (functor_identity _ ) D D'. Proof. use tpair. + intros x xx. exact (pr1 (FF_split x xx)). + intros x y xx yy f ff; simpl. set (Hxx := FF_split x xx). set (Hyy := FF_split y yy). apply FFinv. refine (transportf (mor_disp _ _) _ _). 2: exact ((pr2 Hxx ;; ff) ;; inv_mor_disp_from_z_iso (pr2 Hyy)). cbn. etrans. apply id_right. apply id_left. 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.