proposition: Proposition double_cat_to_predoublecategory_interchange : predoublecategory_interchange double_cat_to_predoublecategory_sq_hor_ver_unit_assoc_data.
proof: Proof. repeat split ; intro ; intros ; cbn. - apply (id_h_square_id (C := C)). - apply (id_h_square_comp (C := C)). - apply (comp_h_square_id (C := C)). - apply (comp_h_square_comp (C := C)). 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