Proposition disp_univalent_2_1_lift_disp_bicat (HD : disp_univalent_2_1 D₂) : disp_univalent_2_1 lift_disp_bicat. 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.
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.