Proposition lr_lwhisker_v_comp_square {B : verity_double_bicat} {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₂) (s₁ : square_double_bicat h₁ h₂ v₁ w₁) (s₂ : square_double_bicat h₂ h₃ v₂ w₂) : (τ₁ ◃s s₁) ⋆v (τ₂ ◃s s₂) = (τ₂ ⋆⋆ τ₁) ◃s s₁ ⋆v s₂. Proof. rewrite l_lwhisker_v_comp_square. rewrite r_lwhisker_v_comp_square. rewrite <- lwhisker_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.