Definition disp_inv2cell_weq_disp_z_iso : disp_invertible_2cell (id2_invertible_2cell f) ff₁ ff₂ ≃ @z_iso_disp _ (disp_hom xx yy) _ _ (identity_z_iso _) ff₁ ff₂. Proof. use make_weq. - exact disp_inv2cell_to_disp_z_iso. - use isweq_iso. + exact disp_z_iso_to_disp_inv2cell. + abstract (intro α ; use subtypePath ; [ intro ; apply isaprop_is_disp_invertible_2cell | ] ; apply idpath). + abstract (intro α ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.