{x002 x012 x102 x112 : A} {p0i2 : x002 = x012} {p00j : x001 = x002} {p01j : x011 = x012} {p1i2 : x102 = x112} {p10j : x101 = x102} {p11j : x111 = x112} {pi02 : x002 = x102} {pi12 : x012 = x112} {s0ij : PathSquare p0i1 p0i2 p00j p01j} {s1ij : PathSquare p1i1 p1i2 p10j p11j} {si0j : PathSquare p00j p10j pi01 pi02} {si1j : PathSquare p01j p11j pi11 pi12} {sii2 : PathSquare p0i2 p1i2 pi02 pi12} (ciij : PathCube s0ij s1ij sii1 sii2 si0j si1j) : PathCube (sq_concat_h s0ii s0ij) (sq_concat_h s1ii s1ij) sii0 sii2 (sq_concat_v si0i si0j) (sq_concat_v si1i si1j). Proof. destruct ciij, p00i, p10i, p11i, p01i. exact ciii. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.