Definition is_z_iso_inv_from_z_iso_disp {C : category} {D : disp_cat_data C} {x y : C} {f : z_iso x y}{xx : D x} {yy : D y} (i : z_iso_disp f xx yy) : is_z_iso_disp (z_iso_inv_from_z_iso f) (inv_mor_disp_from_z_iso i). Proof. use tpair. - change ( xx -->[ z_iso_inv_from_z_iso (z_iso_inv_from_z_iso f)] yy). set (XR := transportb (mor_disp xx yy ) (maponpaths pr1 (z_iso_inv_z_iso_inv _ _ f))). apply XR. apply i. - cbn. split. + abstract ( etrans ;[ apply mor_disp_transportf_postwhisker |]; etrans ; [ apply maponpaths; apply (inv_mor_after_z_iso_disp i) | ]; etrans ;[ apply transport_f_f |]; apply transportf_comp_lemma; apply transportf_comp_lemma_hset; try apply homset_property; apply idpath ). + abstract ( etrans ;[ apply mor_disp_transportf_prewhisker |]; etrans ;[ apply maponpaths; apply (z_iso_disp_after_inv_mor i) |]; etrans ;[ apply transport_f_f |]; apply transportf_comp_lemma; apply transportf_comp_lemma_hset; try apply homset_property; apply idpath ). 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.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core.