Слой кубов

#lang rzk-1

Все кубы находятся во вселенной CUBE.

Есть два встроенных куба:

1. Куб 1 — это единичный куб с единственной точкой *_1
2. Куб 2 — это куб направленного интервала с точками 0_2 и 1_2

Также возможно иметь переменные CUBE и делать произведения кубов:

1. I * J — это произведение кубов I и J
2. (t, s) — это точка в I * J, если t : I и s : J
3. если ts : I * J, то first ts : I и second ts : J

Обычно вы можете использовать (t, s) как в качестве паттерна, так и в качестве конструкции пары точек:

-- Перестановка компонент точки в кубе I × I
#define swap
    ( I : CUBE)
  : ( I × I) → I × I
  := \ (t , s) → (s , t)