{A B : Type} {f g : A -> B} {a1 a2 : A} {p : a1 = a2} {q1 : f a1 = g a1} {q2 : f a2 = g a2} : DPath (fun x => f x = g x) p q1 q2 <~> PathSquare q1 q2 (ap f p) (ap g p). Proof. destruct p. exact sq_G1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.