Definition disp_adjequiv_over_id_weq_lift {x : E} (xx yy : lift_disp_bicat x) : disp_adjoint_equivalence (internal_adjoint_equivalence_identity (pr1 x)) xx yy ≃ disp_adjoint_equivalence (internal_adjoint_equivalence_identity x) xx yy. Proof. use weqfibtototal. intro ff. exact (disp_left_adjoint_equivalence_over_id_weq_lift ff). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Section FromLift. End FromLift.