ap_nat' {A B} {f f' : A -> B} (h : f == f') {x y : A} (p : x = y) : PathSquare (h x) (h y) (ap f p) (ap f' p). Proof. by destruct p; apply sq_G1. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.