proposition: 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₁ ⋆v s₂) ⋆h s₃ = transportf_square (idpath _) (id_v_left _ @ r) ((s₁ ⋆h transportf_square q₁ (idpath _) (id_v_square _)) ⋆v (s₂ ⋆h transportf_square (hcomp_split_globular_l_path q₁ q₂) (!r) s₃)).
proof: Proof. induction q₁, q₂, r. rewrite <- comp_h_square_comp. rewrite transportf_square_postwhisker. rewrite transportf_square_prewhisker. rewrite transportf_f_square. rewrite square_id_left_v. unfold transportb_square. rewrite transportf_f_square. rewrite transportf_hcomp_r. rewrite transportf_f_square. rewrite !transportf_square_id. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DoubleCategories.Core.DoubleCats UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws UniMath.Bicategories.DoubleCategories.DerivedLaws.Variations