{a02 a12 : A} {p0y : a01 = a02} {p1y : a11 = a12} {px2 : a02 = a12} : PathSquare px0 px1 p0x p1x -> PathSquare px1 px2 p0y p1y -> PathSquare px0 px2 (p0x @ p0y) (p1x @ p1y). Proof. intros a b. destruct b. refine (sq_ccGG _ _ a). 1,2: apply inverse, concat_p1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.