{A B} (f : A -> B) {a0 a1 : A} (p : a0 = a1) : sq_ap f (sq_refl_v p) = sq_refl_v (ap f p). Proof. by destruct p. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.