Proposition lassociator_v_comp_square'' {B : verity_double_bicat} {w₁ w₂ x₁ x₂ y₁ y₂ z₁ z₂ : B} {hw : w₁ --> w₂} {hx : x₁ --> x₂} {hy : y₁ --> y₂} {hz : z₁ --> z₂} {u₁ : w₁ -|-> x₁} {u₂ : x₁ -|-> y₁} {u₃ : y₁ -|-> z₁} {v₁ : w₂ -|-> x₂} {v₂ : x₂ -|-> y₂} {v₃ : y₂ -|-> z₂} (s₁ : square_double_bicat hw hx u₁ v₁) (s₂ : square_double_bicat hx hy u₂ v₂) (s₃ : square_double_bicat hy hz u₃ v₃) : s₁ ⋆v (s₂ ⋆v s₃) = lassociator u₁ u₂ u₃ ◃s (rassociator v₁ v₂ v₃ ▹s s₁ ⋆v s₂ ⋆v s₃). Proof. rewrite <- rwhisker_lwhisker_square. rewrite lassociator_v_comp_square. rewrite <- rwhisker_square_comp. rewrite lassociator_rassociator. rewrite rwhisker_square_id. 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.