{A : Type} {B : A -> Type} (f g : forall a : A, B a) {x1 x2 : A} (p : x1 = x2) (q1 : f x1 = g x1) (q2 : f x2 = g x2) : DPath (fun x : A => f x = g x) p q1 q2 <~> DPathSquare B (sq_refl_h p) (apD f p) (apD g p) q1 q2. Proof. destruct p. exact sq_1G. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.