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