q = q' <~> PathSquare 1 1 q q' := sq_path oE equiv_1p_q1 oE equiv_path_inverse _ _.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.