{X} {a b : X} {p q : a = b} : (p = q) <~> (p @ 1 = 1 @ q). Proof. refine (equiv_compose' _ _). - exact (equiv_concat_r (concat_1p _)^ _). - exact (equiv_concat_l (concat_p1 _) _). Defined.
From HoTT Require Import Basics Types.