{A : Type} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} : PathSquare px0 px1 p0x p1x <~> PathSquare px1 px0 p0x^ p1x^. Proof. destruct p0x, p1x. refine (sq_G1 oE _). refine (equiv_path_inverse _ _ oE _). apply sq_G1^-1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.