{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} : sq_concat_h (tr (fv s0ii)) (sq_concat_h si0i (tr s1ii)) = sq_ccGG (moveL_Vp _ _ _ (sq_path^-1 sii0)) (moveL_Vp _ _ _ (sq_path^-1 sii1)) si1i <~> PathCube s0ii s1ii sii0 sii1 si0i si1i. Proof. srapply equiv_adjointify. { destruct sii0, sii1; cbn. rewrite (eisretr sq_G1 si0i)^, (eisretr sq_1G s0ii)^, (eisretr sq_1G s1ii)^. intro X. by destruct (sq_G1^-1 si0i), (sq_1G^-1 s0ii), (sq_1G^-1 s1ii), X, p00i. } 1,2: by intros []. destruct sii0, sii1. cbn. rewrite <- (eisretr sq_G1 si0i). rewrite <- (eisretr sq_1G s0ii). rewrite <- (eisretr sq_1G s1ii). destruct (@equiv_inv _ _ sq_G1 _ si0i). destruct (@equiv_inv _ _ sq_1G _ s0ii). destruct (@equiv_inv _ _ sq_1G _ s1ii). destruct p00i. intro X. by destruct X. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.