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