PathSquare px0 px1 p0x p1x <~> PathSquare p0x^ p1x^ px1 px0. Proof. refine (sq_path oE _). refine (equiv_moveR_Vp _ _ _ oE _). refine (equiv_concat_r (concat_pp_p _ _ _) _ oE _). refine (equiv_moveL_pV _ _ _ oE _). exact sq_path^-1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.