proposition: Proposition to_disp_left_adjoint_equivalence_over_id_lift_axioms : disp_left_adjoint_axioms (internal_adjoint_equivalence_identity x) to_disp_left_adjoint_equivalence_over_id_lift_data.
proof: Proof. split. - refine (pr112 Hff @ _). rewrite lift_transportb. apply maponpaths_2. apply cellset_property. - refine (pr212 Hff @ _). rewrite lift_transportb. apply maponpaths_2. apply cellset_property. 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