Definition double_bicat_interchange_law (B : ver_bicat_sq_id_comp_whisker) : UU := ∏ (x₁ x₂ x₃ y₁ y₂ y₃ z₁ z₂ z₃ : B) (v₁ : x₁ -|-> x₂) (v₁' : x₂ -|-> x₃) (v₂ : y₁ -|-> y₂) (v₂' : y₂ -|-> y₃) (v₃ : z₁ -|-> z₂) (v₃' : z₂ -|-> z₃) (h₁ : x₁ --> y₁) (h₂ : y₁ --> z₁) (k₁ : x₂ --> y₂) (k₂ : y₂ --> z₂) (l₁ : x₃ --> y₃) (l₂ : y₃ --> z₃) (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₁' : square_double_bicat k₁ l₁ v₁' v₂') (s₂ : square_double_bicat h₂ k₂ v₂ v₃) (s₂' : square_double_bicat k₂ l₂ v₂' v₃'), (s₁ ⋆v s₁') ⋆h (s₂ ⋆v s₂') = (s₁ ⋆h s₂) ⋆v (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.