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. exact (pr1 (pr122 (pr222 (pr12 B))) _ _ _ _ τ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.