Proposition disp_left_adjoint_equivalence_over_id_weq_lift_right (Hff : disp_left_adjoint_equivalence (internal_adjoint_equivalence_identity x) ff) : to_disp_left_adjoint_equivalence_over_id_lift (from_disp_left_adjoint_equivalence_over_id_lift Hff) = Hff. Proof. use subtypePath. { intro. use isapropdirprod. - use isapropdirprod ; apply disp_cellset_property. - use isapropdirprod ; use isaprop_is_disp_invertible_2cell. } apply idpath. Qed.
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.