Направленный интервал

Куб 2 — это направленный интервал, который является основой синтетической теории ∞-категорий.

#lang rzk-1

Точки направленного интервала

Направленный интервал 2 имеет две точки:

• 0_2 — начальная точка (источник)
• 1_2 — конечная точка (цель)

Неравенство

Направленный интервал поддерживает топ неравенства <= (или ≤):

• t <= s — это топ, который выполняется, когда t : 2 и s : 2 и t меньше или равно s в направленном порядке

Это неравенство используется для определени симплексов и для выражения направленности в синтетической теории ∞-категорий.

Пример

-- 2-симплекс использует неравенство, чтобы оставить только половину квадрата
#define Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

Примечания

• Направленный интервал 2 отличается от единичного куба 1
• Произведения кубов 2 (такие как 2 × 2) используются для определения многомерных форм
• Неравенство ≤ валидно только для точек куба 2