Proposition hcomp_split_globular_l'_idpath {C : double_cat} {x y z : C} {u₁ u₂ : x -->v x} (q : identity_v y ·v identity_v y = identity_v y) {h₁ h₂ h₃ : x -->h y} {k₁ k₂ : y -->h z} (s₁ : square u₁ (identity_v y) h₁ h₂) (s₂ : square u₂ (identity_v y) h₂ h₃) (s₃ : square (identity_v y ·v identity_v y) (identity_v z) k₁ k₂) : (s₁ ⋆h id_v_square _) ⋆v (s₂ ⋆h transportf_square q (idpath _) s₃) = transportb_square (idpath _) (id_v_left _) ((s₁ ⋆v s₂) ⋆h s₃). Proof. refine (_ @ hcomp_split_globular_l' (idpath _) (idpath _) (idpath _) s₁ s₂ s₃ @ _). - do 2 apply maponpaths. use transportf_square_eq. apply idpath. - use transportf_square_eq. 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.