proposition: Proposition to_disp_left_adjoint_equivalence_over_id_lift_inv : disp_left_equivalence_axioms (internal_adjoint_equivalence_identity x) to_disp_left_adjoint_equivalence_over_id_lift_data.
proof: Proof. split. - pose (H := pr122 Hff). simple refine (_ ,, _ ,, _). + exact (pr1 H). + refine (pr12 H @ _). rewrite lift_transportb. apply maponpaths_2. apply cellset_property. + refine (pr22 H @ _). rewrite lift_transportb. apply maponpaths_2. apply cellset_property. - pose (H := pr222 Hff). simple refine (_ ,, _ ,, _). + exact (pr1 H). + refine (pr12 H @ _). rewrite lift_transportb. apply maponpaths_2. apply cellset_property. + refine (pr22 H @ _). 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