{A B C} (f : A -> B -> C) {a a' : A} (p : a = a') {b b' : B} (q : b = b') : PathSquare (ap (fun x => f x b) p) (ap (fun x => f x b') p) (ap (f a) q) (ap (f a') q). Proof. apply sq_dp. exact (apD (fun y => ap (fun x => f x y) p) q). Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.