Definition p1types_disp : disp_bicat one_types. Proof. use tpair. - apply p1types_prebicat. - repeat intro. apply hlevelntosn. apply one_type_isofhlevel. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.