Directed interval cube

The 2 cube is the directed interval, which is a fundamental building block for synthetic ∞-category theory.

#lang rzk-1

Points

The directed interval 2 has two points:

• 0_2 — the initial point (source)
• 1_2 — the terminal point (target)

Inequality

The directed interval supports an inequality tope <= (or ≤):

• t <= s is a tope that is satisfied when t : 2 and s : 2 and t is less than or equal to s in the directed ordering

This inequality is used to define shapes like simplices and to express directedness in synthetic ∞-category theory.

Example

-- A 2-simplex uses the inequality to take only half of the square
#define Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

Notes

• The directed interval 2 is distinct from the unit cube 1
• Products of 2 cubes (like 2 × 2) are used to define higher-dimensional shapes
• The inequality ≤ is only valid for points of cube 2