{A} {a0 a1 : A} (p : a0 = a1) : PathSquare 1 1 p p := sq_1G 1.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.