Proposition hcomp_l_inj {C : double_cat} {x y z : C} {g : x -->h y} {h : x -->h z} {v : y -->v z} {v' : x -->v x} {s s' : square v' v g h} (p : identity_v x = v') (q : id_v_square (identity_h _) ⋆h (transportf_square (!p) (idpath _) s) = id_v_square (identity_h x) ⋆h (transportf_square (!p) (idpath _) s')) : s = s'. Proof. induction p ; cbn in q. refine (!(square_id_left_v' _) @ _ @ square_id_left_v' _). apply maponpaths. rewrite <- linvunitor_lunitor_h'. rewrite !transportf_square_prewhisker. apply maponpaths. refine (!(square_assoc_v' _ _ _) @ _ @ square_assoc_v' _ _ _). do 2 apply maponpaths. rewrite <- !lunitor_square'. apply maponpaths. apply maponpaths_2. rewrite !id_h_square_id. exact q. 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.