{px0 : a00 = a10} {p0x : a00 = a01} {p1x : a10 = a11} {px1 : a01 = a11} (s : PathSquare px0 px1 p0x p1x) {px1' : a01 = a11} (s' : PathSquare px0 px1' p0x p1x) : px1 = px1'. Proof. destruct s. apply sq_path^-1 in s'. exact (s' @ concat_1p _). Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.