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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.AlternativeDefinitions.DoubleCatsUnfolded.