(t0ii : DPathSquare P s0ii q0i0 q0i1 q00i q01i) (t1ii : DPathSquare P s1ii q1i0 q1i1 q10i q11i) (tii0 : DPathSquare P sii0 q0i0 q1i0 qi00 qi10) (tii1 : DPathSquare P sii1 q0i1 q1i1 qi01 qi11) (ti1i : DPathSquare P si1i q01i q11i qi10 qi11) : {ti0i : DPathSquare P si0i q00i q10i qi00 qi01 & DPathCube P c t0ii t1ii tii0 tii1 ti0i ti1i}. Proof. destruct c. apply cu_fill_front. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Cubical.PathCube.