proposition: Proposition lassociator_h_comp_square'' {B : verity_double_bicat} {x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : B} {h₁ : x₁ --> x₂} {h₂ : x₂ --> x₃} {h₃ : x₃ --> x₄} {k₁ : y₁ --> y₂} {k₂ : y₂ --> y₃} {k₃ : y₃ --> y₄} {v₁ : x₁ -|-> y₁} {v₂ : x₂ -|-> y₂} {v₃ : x₃ -|-> y₃} {v₄ : x₄ -|-> y₄} (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₂ : square_double_bicat h₂ k₂ v₂ v₃) (s₃ : square_double_bicat h₃ k₃ v₃ v₄) : s₁ ⋆h s₂ ⋆h s₃ = lassociator k₁ k₂ k₃ ▿s (rassociator h₁ h₂ h₃ ▵s s₁ ⋆h (s₂ ⋆h s₃)).
proof: Proof. rewrite dwhisker_uwhisker_square. rewrite lassociator_h_comp_square. rewrite <- uwhisker_square_comp. rewrite rassociator_lassociator. rewrite uwhisker_square_id. 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.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat