proposition: Lemma total_is_univalent_2 {C : bicat} {D: disp_bicat C} : disp_univalent_2 D → is_univalent_2 C → is_univalent_2 (total_bicat D).
proof: Proof. intros UD UC. split. - apply total_is_univalent_2_0. { apply UC. } apply disp_univalent_2_0_of_2. assumption. - apply total_is_univalent_2_1. { apply UC. } apply disp_univalent_2_1_of_2. assumption. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.AdjointUnique UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions