{A} {P : A -> Type} {f g : forall x, P x} {x y : A} (q : f == g) (p : x = y) : DPathSquare P (sq_refl_h _) (apD f p) (apD g p) (q x) (q y). Proof. destruct p. by apply sq_1G. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.