Слой кубов

#lang rzk-1

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

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

1. Куб 1 — это единичный куб с единственной точкой *_1
2. Куб 2 — это куб направленного интервала с точками 0_2 и 1_2, с линейным порядком
3. Куб 𝕀 (или II в ASCII) — дедекиндов кубический интервал с точками 0ᵢ и 1ᵢ, без тотального порядка

2 является подтипом 𝕀: любая точка 2 может использоваться там, где ожидается 𝕀. Кубический интервал 𝕀 используется аналогично 2, но без тотального порядка:

-- Кубический hom-тип в A между x и y
#define cub-hom
  (A : U) (x y : A)
  : U
  := (t : II) -> A [ t === 0_I |-> x , t === 1_I |-> y ]

Также возможно иметь переменные 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)