Cube layer

#lang rzk-1

All cubes live in CUBE universe.

There are two 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

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)