Proposition disp_prebicat_laws_on_cat_to_univ_cat : disp_prebicat_laws disp_prebicat_data_on_cat_to_univ_cat. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor.