PathSquare px0 px1 p0x p1x <~> PathSquare px1^ px0^ p1x^ p0x^. Proof. refine (sq_path oE _ ). refine (equiv_concat_lr (inv_pp _ _)^ (inv_pp _ _) oE _). refine (equiv_ap _ _ _ oE _). refine (sq_path^-1 oE _). exact sq_tr. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.