PathSquare px0 px1 p0x p1x <~> PathCube (sq_1G px0) (sq_1G px1) 1 1 (sq_G1 p0x) (sq_G1 p1x). Proof. destruct p0x, p1x, a10. refine(_ oE sq_G1^-1). refine (_ oE equiv_ap' sq_1G _ _). exact cu_G11. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.