Definition comp_cylinder_law (B : ver_bicat_sq_id_comp_whisker) : UU := (∏ (x₁ x₂ y₁ y₂ z₁ z₂ : B) (h₁ : x₁ --> x₂) (h₂ : y₁ --> y₂) (h₃ : z₁ --> z₂) (v₁ v₁' : x₁ -|-> y₁) (v₂ v₂' : y₁ -|-> z₁) (w₁ w₁' : x₂ -|-> y₂) (w₂ w₂' : y₂ -|-> z₂) (τ₁ : v₁ =|=> v₁') (τ₂ : v₂ =|=> v₂') (θ₁ : w₁ =|=> w₁') (θ₂ : w₂ =|=> w₂') (s₁ : square_double_bicat h₁ h₂ v₁ w₁) (s₁' : square_double_bicat h₁ h₂ v₁' w₁') (s₂ : square_double_bicat h₂ h₃ v₂ w₂) (s₂' : square_double_bicat h₂ h₃ v₂' w₂') (p : is_ver_cylinder s₁ s₁' τ₁ θ₁) (q : is_ver_cylinder s₂ s₂' τ₂ θ₂), is_ver_cylinder (s₁ ⋆v s₂) (s₁' ⋆v s₂') (τ₁ ⋆ τ₂) (θ₁ ⋆ θ₂)) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ : B) (h₁ h₁' : x₁ --> x₂) (h₂ h₂' : x₂ --> x₃) (k₁ k₁' : y₁ --> y₂) (k₂ k₂' : y₂ --> y₃) (v₁ : x₁ -|-> y₁) (v₂ : x₂ -|-> y₂) (v₃ : x₃ -|-> y₃) (τ₁ : h₁ ==> h₁') (τ₂ : h₂ ==> h₂') (θ₁ : k₁ ==> k₁') (θ₂ : k₂ ==> k₂') (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₂' : square_double_bicat h₂' k₂' v₂ v₃) (p : is_hor_cylinder s₁ s₁' τ₁ θ₁) (q : is_hor_cylinder s₂ s₂' τ₂ θ₂), is_hor_cylinder (s₁ ⋆h s₂) (s₁' ⋆h s₂') (τ₁ ⋆ τ₂) (θ₁ ⋆ θ₂)).
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.