Proposition ver_bicat_hcomp_v_comp_square {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 : τ₁ ◃s s₁' = θ₁ ▹s s₁) (q : τ₂ ◃s s₂' = θ₂ ▹s s₂) : (τ₂ ⋆⋆ τ₁) ◃s s₁' ⋆v s₂' = (θ₂ ⋆⋆ θ₁) ▹s s₁ ⋆v s₂. Proof. exact (pr1 (pr222 (pr1 (pr222 B))) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ p q). 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.