{A P : Type} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} {s : PathSquare px0 px1 p0x p1x} {b00 b10 b01 b11 : P} {qx0 : b00 = b10} {qx1 : b01 = b11} {q0x : b00 = b01} {q1x : b10 = b11} : PathSquare qx0 qx1 q0x q1x <~> DPathSquare (fun _ => P) s (dp_const qx0) (dp_const qx1) (dp_const q0x) (dp_const q1x). Proof. by destruct s. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.