Proposition disp_univalent_2_0_lift_disp_bicat (HD₁ : disp_univalent_2_0 D₂) (HD₂ : disp_univalent_2_1 D₂) (HB : is_univalent_2_1 B) (HD' : disp_univalent_2_1 D₁) : disp_univalent_2_0 lift_disp_bicat. Proof. use fiberwise_univalent_2_0_to_disp_univalent_2_0. intros x xx yy. use weqhomot. - exact (disp_adjequiv_over_id_weq_lift xx yy ∘ make_weq _ (HD₁ _ _ (idpath _) xx yy))%weq. - intro p ; cbn in p. induction p. use subtypePath. { intro. use (isaprop_disp_left_adjoint_equivalence). - exact (total_is_univalent_2_1 _ HB HD'). - use disp_univalent_2_1_lift_disp_bicat. exact HD₂. } cbn. 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.