{A : Type} (x y : A) : (x = y) <~> (y = x) := Build_Equiv _ _ (@inverse A x y) _. Global Instance isequiv_concat_l {A : Type} `(p : x = y:>A) (z : A) : IsEquiv (@transitivity A _ _ x y z p) | 0. Proof. refine (Build_IsEquiv _ _ _ (concat p^) (concat_p_Vp p) (concat_V_pp p) _). intros q; destruct p; destruct q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.