Definition disp_idtoiso_2_0_isotoid_2_0 {B : bicat} {D : disp_bicat B} (HD_2_0 : disp_univalent_2_0 D) {x : B} {xx yy : D x} (ee : disp_adjoint_equivalence (internal_adjoint_equivalence_identity x) xx yy) : disp_idtoiso_2_0 D (idpath _) xx yy (disp_isotoid_2_0 HD_2_0 ee) = ee. Proof. exact (homotweqinvweq (make_weq _ (HD_2_0 x x (idpath _) xx yy)) ee). 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.