{px0' px1' p0x' p1x'} (qx0 : px0 = px0') (qx1 : px1 = px1') (q0x : p0x = p0x') (q1x : p1x = p1x') : PathSquare px0 px1 p0x p1x <~> PathSquare px0' px1' p0x' p1x'. Proof. by destruct qx0, qx1, q0x, q1x. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.