Dan

General Algebra Processing (Dan), 1-Categories (Mike), and ∞-Categories (Ulrik) in a unified simplicial HoTT environment by 5HT.

Abstract

We present a domain-specific language (DSL) ecosystem linking the operational, computer-algebraic core (Dan) with the theoretical proof assistants Mike (Directed Type Theory) and Ulrik (Simplicial Type Theory). Designed as a fast type checker with a focus on algebraic purity, the system employs a Lean/Anders-like sequent syntax to define k-dimensional simplices, categories, and spectra via explicit contexts, vertex lists, and face relations.

By balancing algebraic simplicity with practical efficiency, the system avoids complex path-filling (e.g. PathP) at the surface, enabling linear-time combinatorial checks at the operational layer. High-level objects are elaborated and translated directly to type theory, where metatheorems (such as limits, adjunctions, or Yoneda mappings) are proven and verified.

The Three Languages

A tiered approach to simplicial category theory, bridging active computation with formal proof verification.

Dan

General Algebra Processing (GAP)

Dan is a statically checked, presentation-oriented language. It allows programmers and mathematicians to define combinatorial cells, groups, rings, and simplicial complexes, and checks their structural soundness.

Dan maps directly into theoretical engines, proving metatheorems that hold "for free" across all models.

Mike

Directed Type Theory (dirtt)

Mike is a proof assistant based on Directed Type Theory (dirtt) with linear polarities (+/-) and quadraticality constraints. It is tailored for formal 1-category theory.

It represents hom-spaces directly, handling limits/colimits as ends and coends, and maps linear constructs such as tensors ⊗ and linear functions ⊸ to the simplicial core.

Ulrik

Simplicial Type Theory (STT)

Ulrik is a proof assistant based on Riehl-Shulman simplicial type theory (STT). It features a directed interval 𝕀, Segal precategories, and Rezk categories where identity paths and isomorphisms coincide.

It implements modal operators (opposite category, twisted arrow categories) and forms the core checker for synthetic ∞-category theory in compact modal manner.

The Lift: Term Transfer

The lift compiler operates as the translation bridge between the operational layer (Dan) and the theoretical layer (Ulrik and Mike). It compiles low-level algebraic definitions and combinatorial complexes into high-level type-theoretic terms.

1. Parsing

Lexes and parses the .dan source file into the operational AST structure.

➔

2. Spec Folding

Folds sequent hypotheses into dependent products (EPi) and definition boundaries into Sigma types (ESig).

➔

3. Sanitization

Translates mathematical Unicode symbols (e.g. ∂, s₀) into clean, ASCII-safe identifiers.

➔

4. Pretty-Printing

Outputs a verified, type-checkable .ulrik source file.

Case Study: Möbius Strip Representation

Comparison between local combinatorial complexes (Dan) and global synthetic fiber bundles (Anders HoTT).

Attribute Simplicial / Dan Kan (Möbius) Synthetic HoTT (moebius in Anders)
Framework General Computer Algebra (GAP-like) / Simplicial Sets Homotopy Type Theory (HoTT/Cubical)
Mathematical Type A product of Simplex variables and boundary relations A function/fibration: S¹ → U
Homotopy Type Contractible (∗) since it models a single local triangle Homotopy equivalent to a circle (S¹)
Mechanism of Twist Specified algebraically via boundary face compositions in coordinates Specified via univalent path induction (ua) using a boolean negation equivalence
Conceptual Role A local 2-cell configuration (oriented triangular building block) The global non-trivial fiber bundle (the double cover total space)

Connection: glues multiple local Möbius triangles with a twist to form a simplicial set X. Its geometric realization |X| is homeomorphic to the total space of the HoTT fibration ∑_{x : S¹} moebius(x).

Algebraic Presentations in Dan

Sequent definitions declared in the computer algebra core are checked in linear time.

Group presentation: ℤ/3ℤ

Presented by a single generator subject to relation a³ = e. Identity and generators are declared in the context.

def z3 : Group
 := П (e a : Simplex),
      a³ = e
    ⊢ 1 (a | a³ = e)

Monoid presentation: ℕ

Natural numbers defined algebraically as a monoid. Verification checks composition and boundary coherence.

def nat_monoid : Monoid
 := П (z s : Simplex),
      s ∘ z = s, z ∘ s = s
    ⊢ 2 (z s | s ∘ z = s, z ∘ s = s)

Simplicial Circle S¹

Defined by a vertex and edge mapping endpoints to the basepoint. The degeneracy constraint collapses v to an edge.

def circle : Simplicial
 := П (v e : Simplex),
      ∂₁₀ = v, ∂₁₁ = v, s₀ < v
    ⊢ 1 (v, e | ∂₁₀ ∂₁₁, s₀)

Category with Group Symmetries

Nested algebraic structures in the context allow categories to inherit properties from internal groups.

def path_z2_category : Category
 := П (x y : Simplex),
      (f g h : Simplex),
      (z2 : Group(П (e a : Simplex),
      a² = e ⊢ 1 (a | a² = e))),
      f ∘ g = h
    ⊢ 2 (x y | f g h | f ∘ g = h)

The Middle Way

How constructors and types map between the operational and theoretical layers of the ecosystem.

Language Construct AST Node Classification Target Mapping
Dan (GAP) Type Former Category Elaborated Segal Precategory / Type with composition path
Type Former Group Elaborated Classifying Space BG (single-object Segal type)
Constraint Eq / Map Elaborated Strict equality EId or interval ordering ELeq
Ulrik (STT) Type Former EPi / ESig Primitive Dependent function space Π and pair space Σ
Type Former EIDir / ELeq Primitive Interval coordinate space 𝕀 and inequality relation
Type Former hom(x, y) Derived Extension type {f : 𝕀 → A | f0 = x, f1 = y}
Mike (dirtt) Type Former MHom(cat, a, b) Elaborated Simplicial hom type
Type Former MTensor(M, N) Elaborated Simplicial dependent pair space ESig (Σ)
Type Former MEnd / MCoend Elaborated Simplicial Π (for Limits) and Σ (for Colimits)

Open Source

GitHub Logo