fact: Definition whisker_square_comp_square (B : ver_bicat_sq_id_comp_whisker) : UU := (∏ (x₁ x₂ y₁ y₂ z₁ z₂ : B) (h₁ h₁' : x₁ --> x₂) (h₂ : y₁ --> y₂) (h₃ : z₁ --> z₂) (v₁ : x₁ -|-> y₁) (v₂ : y₁ -|-> z₁) (w₁ : x₂ -|-> y₂) (w₂ : y₂ -|-> z₂) (τ : h₁ ==> h₁') (s₁ : square_double_bicat h₁' h₂ v₁ w₁) (s₂ : square_double_bicat h₂ h₃ v₂ w₂), τ ▵s (s₁ ⋆v s₂) = (τ ▵s s₁) ⋆v s₂) × (∏ (x₁ x₂ y₁ y₂ z₁ z₂ : B) (h₁ : x₁ --> x₂) (h₂ : y₁ --> y₂) (h₃ h₃' : z₁ --> z₂) (v₁ : x₁ -|-> y₁) (v₂ : y₁ -|-> z₁) (w₁ : x₂ -|-> y₂) (w₂ : y₂ -|-> z₂) (τ : h₃ ==> h₃') (s₁ : square_double_bicat h₁ h₂ v₁ w₁) (s₂ : square_double_bicat h₂ h₃ v₂ w₂), τ ▿s (s₁ ⋆v s₂) = s₁ ⋆v (τ ▿s s₂)) × (∏ (x₁ x₂ y₁ y₂ z₁ z₂ : B) (h₁ : x₁ --> x₂) (h₂ h₂' : y₁ --> y₂) (h₃ : z₁ --> z₂) (v₁ : x₁ -|-> y₁) (v₂ : y₁ -|-> z₁) (w₁ : x₂ -|-> y₂) (w₂ : y₂ -|-> z₂) (τ : h₂ ==> h₂') (s₁ : square_double_bicat h₁ h₂ v₁ w₁) (s₂ : square_double_bicat h₂' h₃ v₂ w₂), s₁ ⋆v (τ ▵s s₂) = (τ ▿s s₁) ⋆v s₂) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ : B) (h₁ : x₁ --> x₂) (h₂ : x₂ --> x₃) (k₁ : y₁ --> y₂) (k₂ : y₂ --> y₃) (v₁ v₁' : x₁ -|-> y₁) (v₂ : x₂ -|-> y₂) (v₃ : x₃ -|-> y₃) (τ : v₁ =|=> v₁') (s₁ : square_double_bicat h₁ k₁ v₁' v₂) (s₂ : square_double_bicat h₂ k₂ v₂ v₃), τ ◃s (s₁ ⋆h s₂) = (τ ◃s s₁) ⋆h s₂) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ : B) (h₁ : x₁ --> x₂) (h₂ : x₂ --> x₃) (k₁ : y₁ --> y₂) (k₂ : y₂ --> y₃) (v₁ : x₁ -|-> y₁) (v₂ : x₂ -|-> y₂) (v₃ v₃' : x₃ -|-> y₃) (τ : v₃ =|=> v₃') (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₂ : square_double_bicat h₂ k₂ v₂ v₃), τ ▹s (s₁ ⋆h s₂) = s₁ ⋆h (τ ▹s s₂)) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ : B) (h₁ : x₁ --> x₂) (h₂ : x₂ --> x₃) (k₁ : y₁ --> y₂) (k₂ : y₂ --> y₃) (v₁ : x₁ -|-> y₁) (v₂ v₂' : x₂ -|-> y₂) (v₃ : x₃ -|-> y₃) (τ : v₂ =|=> v₂') (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₂ : square_double_bicat h₂ k₂ v₂' v₃), s₁ ⋆h (τ ◃s s₂) = (τ ▹s s₁) ⋆h s₂).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat