Definition whisker_square_id_square (B : ver_bicat_sq_id_comp_whisker) : UU := (∏ (x y : B) (v w : x -|-> y) (τ : v =|=> w), τ ◃s id_h_square_bicat w = τ ▹s id_h_square_bicat v) × (∏ (x y : B) (h k : x --> y) (τ : h ==> k), τ ▵s id_v_square_bicat k = τ ▿s id_v_square_bicat h).
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.