(s : PathSquare px0 px1 p0x p1x) : PathCube hr hr s s vr vr. Proof. by destruct s. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.