{A : Type} {x y : A} {p q : x = y} : p = q <~> 1 @ p = q @ 1 := equiv_concat_lr (concat_1p p) (concat_p1 q)^. Global Instance isequiv_whiskerL {A} {x y z : A} (p : x = y) {q r : y = z} : IsEquiv (@whiskerL A x y z p q r). Proof. simple refine (isequiv_adjointify _ _ _ _). - apply cancelL. - intros k. unfold cancelL. rewrite !whiskerL_pp. refine ((_ @@ 1 @@ _) @ whiskerL_pVL p k). + destruct p, q; reflexivity. + destruct p, r; reflexivity. - intros k. unfold cancelL. refine ((_ @@ 1 @@ _) @ whiskerL_VpL p k). + destruct p, q; reflexivity. + destruct p, r; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.