Proposition vertical_cell_to_square_comp {x y : B} {v₁ v₂ v₃ : x -|-> y} (τ : v₁ =|=> v₂) (θ : v₂ =|=> v₃) : vertical_cell_to_square (τ • θ) = comp_ver_globular_square (vertical_cell_to_square τ) (vertical_cell_to_square θ). Proof. unfold vertical_cell_to_square, comp_ver_globular_square. rewrite lwhisker_square_comp. rewrite lrwhisker_hcomp_square. rewrite runitor_h_comp_square'. rewrite <- dwhisker_square_comp. rewrite lunitor_runitor_identity. rewrite rinvunitor_runitor. rewrite dwhisker_square_id. rewrite <- uwhisker_square_comp. rewrite runitor_lunitor_identity. rewrite linvunitor_lunitor. rewrite uwhisker_square_id. rewrite rwhisker_lwhisker_square. rewrite <- lwhisker_id_h_square. 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.Unitors. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws.