proposition: Proposition disp_univalent_2_1_lift_disp_bicat (HD : disp_univalent_2_1 D₂) : disp_univalent_2_1 lift_disp_bicat.
proof: Proof. use fiberwise_local_univalent_is_univalent_2_1. intros x y f xx yy ff gg. use weqhomot. - exact (disp_invertible_2cell_over_id_weq_lift ff gg ∘ make_weq _ (HD _ _ _ _ (idpath _) _ _ ff gg))%weq. - intro p ; cbn in p. induction p. use subtypePath. { intro. use isaprop_is_disp_invertible_2cell. } 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