{A} {a b : A} {p : a = b} : sq_tr (sq_refl_v p) = sq_refl_h p. Proof. by destruct p. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.