Proposition hcomp_split_globular_l' {C : double_cat} {x y z : C} {u₁ u₂ : x -->v x} {v₁ v₂ : y -->v y} {w : z -->v z} (q₁ : identity_v y = v₁) (q₂ : identity_v y = v₂) (r : identity_v z = w) {h₁ h₂ h₃ : x -->h y} {k₁ k₂ : y -->h z} (s₁ : square u₁ v₁ h₁ h₂) (s₂ : square u₂ v₂ h₂ h₃) (s₃ : square (v₁ ·v v₂) w k₁ k₂) : (s₁ ⋆h transportf_square q₁ (idpath _) (id_v_square _)) ⋆v (s₂ ⋆h transportf_square (hcomp_split_globular_l_path q₁ q₂) (!r) s₃) = transportb_square (idpath _) (id_v_left _ @ r) ((s₁ ⋆v s₂) ⋆h s₃). Proof. rewrite (hcomp_split_globular_l q₁ q₂ r). rewrite transportbf_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.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.Variations. Import TransportSquare.