{a20 a21 : A} {py0 : a10 = a20} {py1 : a11 = a21} {p2x : a20 = a21} : PathSquare px0 px1 p0x p1x -> PathSquare py0 py1 p1x p2x -> PathSquare (px0 @ py0) (px1 @ py1) p0x p2x. Proof. intros a b. destruct b. refine (sq_GGcc _ _ a). 1,2: apply inverse, concat_p1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.