proposition: Proposition transpose_hor_comp_laws : hor_comp_laws transpose_hor_comp_data.
proof: Proof. split ; cbn. - intros x y z v w. rewrite id_h_square_comp. apply idpath. - intros x₁ x₂ x₃ y₁ y₂ y₃ z₁ z₂ z₃ h₁ h₁' h₂ h₂' h₃ h₃' u₁ u₂ v₁ v₂ w₁ w₂ s₁ s₁' s₂ s₂'. rewrite comp_h_square_comp. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats UniMath.Bicategories.DoubleCategories.DerivedLaws