PathSquare px0 px1 p0x p1x -> PathSquare p1x p0x px0^ px1^. Proof. refine (sq_path oE _). refine (equiv_moveL_Vp _ _ _ oE _). refine (equiv_concat_l (concat_p_pp _ _ _) _ oE _). refine (equiv_moveR_pV _ _ _ oE _). exact sq_path^-1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.