Proposition lr_uwhisker_h_comp_square {B : verity_double_bicat} {x₁ x₂ x₃ y₁ y₂ y₃ : B} {h₁ h₁' : x₁ --> x₂} {h₂ h₂' : x₂ --> x₃} {k₁ : y₁ --> y₂} {k₂ : y₂ --> y₃} {v₁ : x₁ -|-> y₁} {v₂ : x₂ -|-> y₂} {v₃ : x₃ -|-> y₃} (τ₁ : h₁' ==> h₁) (τ₂ : h₂' ==> h₂) (s₁ : square_double_bicat h₁ k₁ v₁ v₂) (s₂ : square_double_bicat h₂ k₂ v₂ v₃) : (τ₁ ▵s s₁) ⋆h (τ₂ ▵s s₂) = (τ₂ ⋆⋆ τ₁) ▵s (s₁ ⋆h s₂). Proof. rewrite l_uwhisker_h_comp_square. rewrite r_uwhisker_h_comp_square. rewrite <- uwhisker_square_comp. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat.