PathSquare px0 px1 p0x p1x <~> PathCube (sq_G1 px0) (sq_G1 px1) (sq_G1 p0x) (sq_G1 p1x) 1 1. Proof. destruct p0x, p1x, a00. refine (_ oE sq_G1^-1). refine (_ oE equiv_ap' sq_G1 _ _). 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.