(px0 : a00 = a10) (p0x : a00 = a01) (p1x : a10 = a11) : {px1 : a01 = a11 & PathSquare px0 px1 p0x p1x}. Proof. exists (p0x^ @ px0 @ p1x). by destruct px0, p0x, p1x. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.