{x020 x021 x120 x121 : A} {p0j0 : x010 = x020} {p1j0 : x110 = x120} {p0j1 : x011 = x021} {p1j1 : x111 = x121} {p02i : x020 = x021} {p12i : x120 = x121} {pi20 : x020 = x120} {pi21 : x021 = x121} {s0ji : PathSquare p0j0 p0j1 p01i p02i} {s1ji : PathSquare p1j0 p1j1 p11i p12i} {sij0 : PathSquare p0j0 p1j0 pi10 pi20} {sij1 : PathSquare p0j1 p1j1 pi11 pi21} {si2i : PathSquare p02i p12i pi20 pi21} (ciji : PathCube s0ji s1ji sij0 sij1 si1i si2i) : PathCube (sq_concat_v s0ii s0ji) (sq_concat_v s1ii s1ji) (sq_concat_v sii0 sij0) (sq_concat_v sii1 sij1) si0i si2i. Proof. destruct ciji, p0i0, p1i0, p0i1, p1i1. exact ciii. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.