proposition: Proposition horizontal_cell_to_square_comp {x y : B} {h₁ h₂ h₃ : x --> y} (τ : h₁ ==> h₂) (θ : h₂ ==> h₃) : horizontal_cell_to_square (τ • θ) = comp_hor_globular_square (horizontal_cell_to_square τ) (horizontal_cell_to_square θ).
proof: Proof. unfold horizontal_cell_to_square, comp_hor_globular_square. rewrite uwhisker_square_comp. rewrite ud_whisker_vcomp_square. rewrite runitor_v_comp_square'. rewrite <- rwhisker_square_comp. rewrite lunitor_runitor_identity. rewrite rinvunitor_runitor. rewrite rwhisker_square_id. rewrite <- lwhisker_square_comp. rewrite runitor_lunitor_identity. rewrite linvunitor_lunitor. rewrite lwhisker_square_id. rewrite dwhisker_uwhisker_square. rewrite <- uwhisker_id_v_square. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws