proposition: Proposition disp_left_adjoint_equivalence_over_id_weq_lift_left (Hff : disp_left_adjoint_equivalence (internal_adjoint_equivalence_identity (pr1 x)) ff) : from_disp_left_adjoint_equivalence_over_id_lift (to_disp_left_adjoint_equivalence_over_id_lift Hff) = Hff.
proof: Proof. use subtypePath. { intro. use isapropdirprod. - use isapropdirprod ; apply disp_cellset_property. - use isapropdirprod ; use isaprop_is_disp_invertible_2cell. } apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence