proposition: Proposition lwhisker_id_h_square {x y : B} {v w : x -|-> y} (τ : v =|=> w) : τ ◃s id_h_square_bicat w = τ ▹s id_h_square_bicat v.
proof: Proof. exact (pr1 (pr122 (pr222 (pr12 B))) _ _ _ _ τ). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat