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. 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.
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.