directed-interval

npx skills add majiayu000/claude-skill-registry --skill directed-interval-plurigrid-asi-2 --agent claude-code

Same command for any agent — swap --agent for codex, cursor, copilot.

# Directed Interval Skill > *"The directed interval 2 is the walking arrow: a single morphism 0 → 1."* > — Riehl-Shulman ## Overview The **directed interval 2** replaces the undirected interval 𝕀 of cubical type theory with a directed version. This axiomatizes the notion of "time flows forward" essential for modeling reactions. ## Core Definitions (Rzk) ```rzk #lang rzk-1 -- CUBES: The category of directed cubes -- 2 is the basic directed interval [0 → 1] -- The directed interval (primitive) #define 2 : CUBE -- Endpoints #define 0₂ : 2 #define 1₂ : 2 -- The unique arrow (built-in) -- There is a morphism 0₂ → 1₂ but NOT 1₂ → 0₂ -- Higher cubes built from 2 #define 2×2 : CUBE := 2 × 2 -- Directed square (all arrows point same way) #define □ : CUBE := 2 × 2 -- Simplex shapes #define Δ¹ : CUBE := 2 #define Δ² : CUBE := { (t₁, t₂) : 2 × 2 | t₁ ≤ t₂ } #define Δ³ : CUBE := { (t₁, t₂, t₃) : 2 × 2 × 2 | t₁ ≤ t₂ ∧ t₂ ≤ t₃ } -- Hom type as extension type #define hom (A : U) (x y : A) : U := { f : 2 → A | f 0₂ = x ∧ f 1₂ = y } -- equivalently: (t : 2) → A [t ≡ 0₂ ↦ x, t ≡ 1₂ ↦ y] ``` ## Chemputer Semantics | Directed Cube Concept | Chemical Interpretation | |----------------------|-----------