Proposition lassociator_h_comp_square {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₄) : lassociator k₁ k₂ k₃ ▿s s₁ ⋆h (s₂ ⋆h s₃) = lassociator h₁ h₂ h₃ ▵s s₁ ⋆h s₂ ⋆h s₃. Proof. exact (pr11 (pr1 (pr222 B)) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ s₁ s₂ s₃). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.