proposition: Proposition disp_prebicat_laws_on_cat_to_univ_cat : disp_prebicat_laws disp_prebicat_data_on_cat_to_univ_cat.
proof: Proof. repeat split ; intro ; intros ; cbn. - refine (disp_id2_left _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_id2_right _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vassocr _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_id2 _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_id2_rwhisker _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_vcomp _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_vcomp _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_lunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_runitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lwhisker_lwhisker _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_lwhisker _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rwhisker_rwhisker _ _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_vcomp_whisker _ _ _ _ _ _ _ _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lunitor_linvunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_linvunitor_lunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_runitor_rinvunitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rinvunitor_runitor _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lassociator_rassociator _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_rassociator_lassociator _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_runitor_rwhisker _ _ @ _). apply maponpaths_2. apply cellset_property. - refine (disp_lassociator_lassociator _ _ _ _ @ _). apply maponpaths_2. apply cellset_property. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.DispPseudofunctor