{A} {x000 x010 x100 x110 x001 x011 x101 x111 : A} {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100} {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111} {pi01 : x001 = x101} {pi11 : x011 = x111} {p00i : x000 = x001} {p01i : x010 = x011} {p10i : x100 = x101} {p11i : x110 = x111} {s0ii : PathSquare p0i0 p0i1 p00i p01i} {s1ii : PathSquare p1i0 p1i1 p10i p11i} {sii0 : PathSquare p0i0 p1i0 pi00 pi10} {sii1 : PathSquare p0i1 p1i1 pi01 pi11} {si0i : PathSquare p00i p10i pi00 pi01} {si1i : PathSquare p01i p11i pi10 pi11} : PathCube s0ii s1ii sii0 sii1 si0i si1i <~> PathCube s1ii s0ii (sq_flip_h sii0) (sq_flip_h sii1) (sq_flip_h si0i) (sq_flip_h si1i). Proof. destruct si1i, si0i. refine (cu_GGcccc _ _ oE _). 1,2: exact (eisretr sq_G1 _). refine (cu_GG1 oE _). refine (sq_flip_h oE _). refine (cu_GG1^-1 oE _). refine (cu_GGGGcc _ _ _ _). all: exact (eisretr sq_G1 _)^. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.