Definition p1types_prebicat : disp_prebicat one_types. Proof. use tpair. - exists p1types_disp_prebicat_1_id_comp_cells. apply p1types_disp_prebicat_ops. - repeat split; repeat intro; 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.