Proposition double_bicat_interchange {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₂'). Proof. exact (pr1 (pr122 B) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ s₁ 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.