{A : Type} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} : DPath (fun xy => fst xy = snd xy) (path_prod' p0x p1x) px0 px1 <~> PathSquare px0 px1 p0x p1x. Proof. refine (_ oE (dp_paths_FlFr _ _ _)^-1). refine (_ oE (equiv_concat_l (concat_pp_p _ _ _) _)^-1). refine (_ oE equiv_moveL_Mp _ _ _). refine (_ oE sq_path). exact (sq_ccGG (ap_fst_path_prod _ _) (ap_snd_path_prod _ _)). Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.