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