equiv_ds_const' {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 : DPath (fun _ => P) px0 b00 b10} {qx1 : DPath (fun _ => P) px1 b01 b11} {q0x : DPath (fun _ => P) p0x b00 b01} {q1x : DPath (fun _ => P) p1x b10 b11} : PathSquare (dp_const^-1 qx0) (dp_const^-1 qx1) (dp_const^-1 q0x) (dp_const^-1 q1x) <~> DPathSquare (fun _ => P) s qx0 qx1 q0x q1x. Proof. by destruct s. Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.