{A} {x y : A} (p : x = y) : PathSquare (ap idmap p) p 1 1 := sq_G1 (ap_idmap p).
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.