Definition associator_cylinder_law (B : ver_bicat_sq_id_comp_whisker) : UU := (∏ (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₄), is_hor_cylinder (s₁ ⋆h (s₂ ⋆h s₃)) ((s₁ ⋆h s₂) ⋆h s₃) (lassociator _ _ _) (lassociator _ _ _)) × (∏ (w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ : B) (hw : w₁ --> w₂) (hx : x₁ --> x₂) (hy : y₁ --> y₂) (hz : z₁ --> z₂) (u₁ : w₁ -|-> x₁) (u₂ : x₁ -|-> y₁) (u₃ : y₁ -|-> z₁) (v₁ : w₂ -|-> x₂) (v₂ : x₂ -|-> y₂) (v₃ : y₂ -|-> z₂) (s₁ : square_double_bicat hw hx u₁ v₁) (s₂ : square_double_bicat hx hy u₂ v₂) (s₃ : square_double_bicat hy hz u₃ v₃), is_ver_cylinder (s₁ ⋆v (s₂ ⋆v s₃)) ((s₁ ⋆v s₂) ⋆v s₃) (lassociator _ _ _) (lassociator _ _ _)).
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.