```\import Paths

-- | The type of squares with a specified boundary
\func Cube2 {A : \Type} {a00 a01 a10 a11 : A}
(p_0 : a00 = a10) -- top edge
(p_1 : a01 = a11) -- bottom edge
(p0_ : a00 = a01) -- left edge
(p1_ : a10 = a11) -- right edge
=> Path (\lam j => p0_ @ j = p1_ @ j) p_0 p_1
\where {
{- | The type of cubes in {A} is equivalent to a certain 2-path in {A}.
-   This function satisfies the following equality:
-   ```equality p q idp idp r == idpe \Type (p = q)```
-}
\func equality (p_0 : a00 = a10) (p_1 : a01 = a11) (p0_ : a00 = a01) (p1_ : a10 = a11)
: (p_0 = p0_ <* p_1 *> inv p1_) = Cube2 p_0 p_1 p0_ p1_
=> path (\lam i => Path (\lam j => p0_ @ I.squeeze i j = p1_ @ I.squeeze i j) p_0 (path (p0_ @ I.squeezeR i __) <* p_1 *> inv (path (p1_ @ I.squeezeR i __))))

{- | This function satisfies the following equality:
-   ```map p q idp idp r == r```
-}
\func map (p_0 : a00 = a10) (p_1 : a01 = a11) (p0_ : a00 = a01) (p1_ : a10 = a11)
(r : p_0 = p0_ <* p_1 *> inv p1_) : Cube2 p_0 p_1 p0_ p1_
=> coe (equality p_0 p_1 p0_ p1_ @) r right
}

\func Cube3 {A : \Type} {v000 v001 v010 v011 v100 v101 v110 v111 : A}
{e00_ : v000 = v100} {e10_ : v001 = v101} {e01_ : v010 = v110} {e11_ : v011 = v111}
{e0_0 : v000 = v010} {e1_0 : v001 = v011} {e0_1 : v100 = v110} {e1_1 : v101 = v111}
{e_00 : v000 = v001} {e_10 : v010 = v011} {e_01 : v100 = v101} {e_11 : v110 = v111}
(f__0 : Cube2 e_00 e_10 e0_0 e1_0) -- back face
(f__1 : Cube2 e_01 e_11 e0_1 e1_1) -- front face
(f_0_ : Cube2 e_00 e_01 e00_ e10_) -- top face
(f_1_ : Cube2 e_10 e_11 e01_ e11_) -- bottom face
(f0__ : Cube2 e0_0 e0_1 e00_ e01_) -- left face
(f1__ : Cube2 e1_0 e1_1 e10_ e11_) -- right face
=> Path (\lam k => Path (\lam j => f0__ @ k @ j = f1__ @ k @ j) (f_0_ @ k) (f_1_ @ k)) f__0 f__1
```