proposition: Proposition double_cat_to_has_predoublecategory_sq_hor_ver_unit_assoc : has_predoublecategory_sq_hor_ver_unit_assoc double_cat_to_predoublecategory_sq_hor_ver_data.
proof: Proof. repeat split. - intros x y f. simple refine (_ ,, _ ,, _ ,, _) ; cbn. + exact (lunitor_h f). + exact (linvunitor_h f). + exact (lunitor_linvunitor_h f). + exact (linvunitor_lunitor_h f). - intros x y f. simple refine (_ ,, _ ,, _ ,, _) ; cbn. + exact (runitor_h f). + exact (rinvunitor_h f). + exact (runitor_rinvunitor_h f). + exact (rinvunitor_runitor_h f). - intros w x y z f g h. simple refine (_ ,, _ ,, _ ,, _) ; cbn. + exact (lassociator_h f g h). + exact (rassociator_h f g h). + exact (lassociator_rassociator_h f g h). + exact (rassociator_lassociator_h f g h). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.AlternativeDefinitions.DoubleCatsUnfolded