Definition p1types_disp_prebicat_1_id_comp_cells : disp_prebicat_1_id_comp_cells one_types. Proof. use tpair. - use tpair. + use tpair. * exact (λ X, pr1 X). * exact (λ _ _ x y f, f x = y). + use tpair. * exact (λ _ _, idpath _). * exact (λ _ _ _ f g x y z Hf Hg, maponpaths g Hf @ Hg). - exact (λ _ _ _ _ α x y ff gg, ff = α x @ gg). 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.