\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