Cube layer

#lang rzk-1

All cubes live in CUBE universe.

There are three built-in cubes:

1. 1 cube is a unit cube with a single point *_1
2. 2 cube is a directed interval cube with points 0_2 and 1_2, equipped with a linear order
3. 𝕀 (or II in ASCII) is a Dedekind cubical interval with points 0ᵢ and 1ᵢ, without a total order

2 is a subtype of 𝕀: any point of 2 can be used where 𝕀 is expected. The cubical interval 𝕀 can be used similarly to 2, but without a total order:

-- A cubical hom-type in A between x and y
#define cub-hom
  (A : U) (x y : A)
  : U
  := (t : II) -> A [ t === 0_I |-> x , t === 1_I |-> y ]

It is also possible to have CUBE variables and make products of cubes:

1. I * J is a product of cubes I and J
2. (t, s) is a point in I * J if t : I and s : J
3. if ts : I * J, then first ts : I and second ts : J

You can usually use (t, s) both as a pattern, and a construction of a pair of points:

-- Swap point components of a point in a cube I × I
#define swap
    ( I : CUBE)
  : ( I × I) → I × I
  := \ ( t , s) → (s , t)