proposition: Lemma p1types_univalent_2 : is_univalent_2 p1types.
proof: Proof. apply total_is_univalent_2. - apply p1types_disp_univalent_2. - apply one_types_is_univalent_2. Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.OneTypes UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence