Dan Kan: Simplicial HoTT

Groupoid Infinity Simplicial HoTT Computer Algebra System is a pure algebraїc implementation with explicit syntaxt for fastest type checking. It supports following extensions: Chain, Cochain, Simplex, Simplicial, Category, Monoid, Group, Ring. Simplicial HoTT is a Rezk/GAP replacement incorporated into CCHM/CHM/HTS Agda-like Anders/Dan with Kan, Rezk and Segal simplicial modes for computable ∞-categories.

Abstract

We present a domain-specific language (DSL), the extension to Cubical Homotopy Type Theory (CCHM) for simplicial structures, designed as a fast type checker with a focus on algebraic purity. Built on the Cohen-Coquand-Huber-Mörtberg (CCHM) framework, our DSL employs a Lean/Anders-like sequent syntax П (context) ⊢ k (v₀, ..., vₖ | f₀, ..., fₗ | ... ) to define k-dimensional 0, ..., n, ∞ simplices via explicit contexts, vertex lists, and face relations, eschewing geometric coherence terms in favor of compositional constraints (e.g., f = g ∘ h). The semantics, formalized as inference rules in a Martin-Löf Type Theory MLTT-like setting, include Formation, Introduction, Elimination, Composition, Computational, and Uniqueness rules, ensuring a lightweight, deterministic computational model with linear-time type checking (O(k + m + n), where k is vertices, m is faces, and n is relations). Inspired by opetopic purity, our system avoids cubical path-filling (e.g., PathP), aligning with syntactic approaches to higher structures while retaining CCHM’s type-theoretic foundation. Compared to opetopic sequent calculi and the Rzk prover, our DSL balances algebraic simplicity with practical efficiency, targeting simplicial constructions over general ∞-categories, and achieves a fast, pure checker suitable for formal proofs and combinatorial reasoning.

Setup

$ ocamlopt -o dan src/simplicity.ml && ./dan

Syntax

Incorporating into CCHM/CHM/HTS Anders/Dan core.

Definition

New sequent contruction:

def <name> : <type> := П (context), conditions ⊢ <n> (elements | constraints)

Instances:

def chain : Chain := П (context), conditions ⊢ n (C₀, C₁, ..., Cₙ | ∂₀, ∂₁, ..., ∂ₙ₋₁)
def simplicial : Simplicial := П (context), conditions ⊢ n (s₀, s₁, ..., sₙ | facemaps, degeneracies)
def group : Group := П (context), conditions ⊢ n (generators | relations)
def cat : Category := П (context), conditions ⊢ n (objects | morphisms | coherence)

BNF

<program> ::= <definition> | <definition> <program>
<definition> ::= "def" <id> ":" <type-name> ":=" <type-term>
<type-name> ::= "Simplex" | "Simplicial" | "Chain" | "Cochain"
                          | "Category"  | "Group" | "Monoid" | "Ring" | "Field"
<type-term> ::= "П" "(" <context> ")" "⊢" <n> "(" <elements> "|" <constraints> ")"
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<superscript> ::= "¹" | "²" | "³" | "⁴" | "⁵" | "⁶" | "⁷" | "⁸" | "⁹"
<n> ::= <digit> | <digit> <n> | "∞"
<context> ::= <hypothesis> | <hypothesis> "," <context>
<hypothesis> ::= <id> ":" <type-term>               % Single declaration, e.g., a : Simplex
               | "(" <id-list> ":" <type-term> ")"  % Grouped declaration, e.g., (a b c : Simplex)
               | <id> "=" <t> "<" <t>               % Map, e.g., ∂₁ = C₂ < C₃
               | <id> "=" <t>                        % Equality, e.g., x = 2
               | <id> "=" <t> "∘" <t>               % Monoid composition, e.g., ac = ab ∘ bc
               | <id> "=" <t> "+" <t>               % Ring addition, e.g., x + y = s
               | <id> "=" <t> "⋅" <t>               % Ring multiplication, e.g., x ⋅ y = p
               | <id> "=" <t> "/" <t>               % Field division, e.g., x / y = d
<id-list> ::= <id> | <id> <id-list>                 % e.g., a b c
<elements> ::= <element-list> | ε
<element-list> ::= <id> | <id> "," <element-list>
<constraints> ::= <constraint-list> | ε
<constraint-list> ::= <constraint> | <constraint> "," <constraint-list>
<constraint> ::= <t> "=" <t>                        % Equality, e.g., a = 2
               | <t> "∘" <t> "=" <t>                % Monoid composition, e.g., a ∘ a = e
               | <t> "+" <t> "=" <t>                % Ring addition, e.g., x + y = s
               | <t> "⋅" <t> "=" <t>                % Ring multiplication, e.g., x ⋅ y = p
               | <t> "/" <t> "=" <t>                % Field division, e.g., x / y = d
               | <id> "<" <id>                      % Map, e.g., ∂₁ < C₂
<t> ::= <id>                                        % e.g., a
      | <t> "∘" <t>                                 % e.g., a ∘ b
      | <t> "+" <t>                                 % e.g., x + y
      | <t> "⋅" <t>                                 % e.g., x ⋅ y
      | <t> "/" <t>                                 % e.g., x / y
      | <t> "^-1"                                   % e.g., a^-1
      | <t> "^" <superscript>                       % e.g., a³
      | "e"                                         % identity
      | <number>                                    % e.g., 2
      | <matrix>                                    % e.g., [[1,2],[3,4]]
<number> ::= <digit> | <digit> <number>             % e.g., 123
<matrix> ::= "[" <row-list> "]"                     % e.g., [[1,2],[3,4]]
<row-list> ::= <row> | <row> "," <row-list>
<row> ::= "[" <number-list> "]"                     % e.g., [1,2]
<number-list> ::= <number> | <number> "," <number-list>  % e.g., 1,2

Meaning of <n> Across Types:

• Simplex: Dimension of the simplex—e.g., n=2 for a triangle (2-simplex).
• Group: Number of generators—e.g., n=1 for Z/3Z (one generator a).
• Simplicial: Maximum dimension of the simplicial set—e.g., n=1 for S1 (up to 1-simplices).
• Chain: Length of the chain (number of levels minus 1)—e.g., n=2 for a triangle chain (0, 1, 2 levels).
• Category: Number of objects—e.g., n=2 for a path category (two objects x,y).
• Monoid: Number of generators—e.g., n=2 for N (zero and successor).

Semantics

Chain

• Formation. Γ ⊢ Chain : Set
• Intro. Γ ⊢ n (S | R) : Chain if Γ = s₀₁, …, sₙₘₙ : Simplex, r₁, …, rₚ ∧ S₀, S₁, …, Sₙ = (s₀₁, …, s₀ₘ₀), …, (sₙ₁, …, sₙₘₙ) ∧ ∀ rⱼ = tⱼ = tⱼ', Γ ⊢ rⱼ : tⱼ = tⱼ' ∧ ∀ ∂ᵢⱼ < sₖₗ, Γ ⊢ ∂ᵢⱼ : sₖₗ → sₖ₋₁,ₘ
• Elim Face. Γ ⊢ ∂ᵢⱼ s : Simplex if Γ ⊢ n (S | R) : Chain ∧ r = ∂ᵢⱼ < s ∧ r ∈ R ∧ s ∈ S
• Comp Face. ∂ᵢⱼ (n (S | R)) → s' if r = ∂ᵢⱼ < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Face. Γ ⊢ ∂ᵢⱼ s ≡ ∂ᵢⱼ s' if Γ ⊢ n (S | R) : Chain ∧ n (S' | R') : Chain ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = ∂ᵢⱼ < s ∈ R ∧ r' = ∂ᵢⱼ < s' ∈ R'

Cochain

• Formation. Γ ⊢ Cochain : Set
• Intro. Γ ⊢ n (S | R) : Cochain if Γ = s₀₁, …, sₙₘₙ : Simplex, r₁, …, rₚ ∧ S₀, S₁, …, Sₙ = (s₀₁, …, s₀ₘ₀), …, (sₙ₁, …, sₙₘₙ) ∧ ∀ rⱼ = tⱼ = tⱼ', Γ ⊢ rⱼ : tⱼ = tⱼ' ∧ ∀ σᵢⱼ < sₖₗ, Γ ⊢ σᵢⱼ : sₖₗ → sₖ₊₁,ₘ
• Elim Degeneracy. Γ ⊢ σᵢⱼ s : Simplex if Γ ⊢ n (S | R) : Cochain ∧ r = σᵢⱼ < s ∧ r ∈ R ∧ s ∈ S
• Comp Degeneracy. σᵢⱼ (n (S | R)) → s' if r = σᵢⱼ < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Degeneracy. Γ ⊢ σᵢⱼ s ≡ σᵢⱼ s' if Γ ⊢ n (S | R) : Cochain ∧ n (S' | R') : Cochain ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = σᵢⱼ < s ∈ R ∧ r' = σᵢⱼ < s' ∈ R'

Category

• Formation. Γ ⊢ Category : Set
• Intro. Γ ⊢ n (O | M | R) : Category if Γ = o₁, …, oₙ, m₁, …, mₖ : Simplex, r₁, …, rₚ ∧ O = (o₁, …, oₙ) ∧ M = (m₁, …, mₙ) ∧ ∀ rⱼ = tⱼ = tⱼ', Γ ⊢ rⱼ : tⱼ = tⱼ' ∧ ∀ tⱼ = mₐ ∘ mᵦ, mₐ, mᵦ ∈ Γ
• Elim Comp. Γ ⊢ c : Simplex if Γ ⊢ n (O | M | R) : Category ∧ r = c = m₁ ∘ m₂ ∧ r ∈ R ∧ m₁, m₂ ∈ Γ
• Comp Comp. (m₁ ∘ m₂) (n (O | M | R)) → c if r = c = m₁ ∘ m₂ ∧ r ∈ R ∧ m₁, m₂ ∈ Γ
• Uniq Comp. Γ ⊢ c ≡ c' if Γ ⊢ n (O | M | R) : Category ∧ n (O' | M' | R') : Category ∧ r = c = m₁ ∘ m₂ ∈ R ∧ r' = c' = m₁' ∘ m₂' ∈ R' ∧ m₁, m₂ ∈ Γ ∧ m₁', m₂' ∈ Γ'

Monoid

• Formation. Γ ⊢ Monoid : Set
• Intro. Γ ⊢ n (M | R) : Monoid if Γ = m₁, …, mₙ : Simplex, r₁, …, rₚ ∧ M = (m₁, …, mₙ) ∧ ∀ rⱼ = tⱼ = tⱼ', Γ ⊢ rⱼ : tⱼ = tⱼ' ∧ ∀ tⱼ = mₐ ∘ mᵦ, mₐ, mᵦ ∈ M
• Elim Comp. Γ ⊢ c : Simplex if Γ ⊢ n (M | R) : Monoid ∧ r = c = m₁ ∘ m₂ ∧ r ∈ R ∧ m₁, m₂ ∈ M
• Comp Comp. (m₁ ∘ m₂) (n (M | R)) → c if r = c = m₁ ∘ m₂ ∧ r ∈ R ∧ m₁, m₂ ∈ M
• Uniq Comp. Γ ⊢ c ≡ c' if Γ ⊢ n (M | R) : Monoid ∧ n (M' | R') : Monoid ∧ r = c = m₁ ∘ m₂ ∈ R ∧ r' = c' = m₁' ∘ m₂' ∈ R' ∧ m₁, m₂ ∈ M ∧ m₁', m₂' ∈ M'

Simplex

• Formation. Γ ⊢ Simplex : Set
• Intro. Γ ⊢ n (S | R) : Simplex if Γ = s₀, …, sₙ : Simplex, r₁, …, rₚ ∧ |S| = n + 1 ∧ ∀ rⱼ = tⱼ = tⱼ', Γ ⊢ rⱼ : tⱼ = tⱼ' ∧ ∀ ∂ᵢ < sₖ, Γ ⊢ ∂ᵢ : sₖ → sₖ₋₁ ∧ ∀ σᵢ < sₖ, Γ ⊢ σᵢ : sₖ → sₖ₊₁
• Elim Face. Γ ⊢ ∂ᵢ s : Simplex if Γ ⊢ n (S | R) : Simplex ∧ r = ∂ᵢ < s ∧ r ∈ R ∧ s ∈ S
• Elim Degeneracy. Γ ⊢ σᵢ s : Simplex if Γ ⊢ n (S | R) : Simplex ∧ r = σᵢ < s ∧ r ∈ R ∧ s ∈ S
• Comp Face. ∂ᵢ (n (S | R)) → s' if r = ∂ᵢ < s' ∧ r ∈ R ∧ s' ∈ S
• Comp Degeneracy. σᵢ (n (S | R)) → s' if r = σᵢ < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Face. Γ ⊢ ∂ᵢ s ≡ ∂ᵢ s' if Γ ⊢ n (S | R) : Simplex ∧ n (S' | R') : Simplex ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = ∂ᵢ < s ∈ R ∧ r' = ∂ᵢ < s' ∈ R'
• Uniq Degeneracy. Γ ⊢ σᵢ s ≡ σᵢ s' if Γ ⊢ n (S | R) : Simplex ∧ n (S' | R') : Simplex ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = σᵢ < s ∈ R ∧ r' = σᵢ < s' ∈ R'

Simplicial

Simplicial Modes

• Γ ⊢ Δₙ : Type (Simplex)
• Γ ⊢ Δₙᵏᵃⁿ : Type
• Γ ⊢ Δₙʳᵉᶻᵏ : Type
• Γ ⊢ Δₙˢᵉᵍᵃˡ : Type

Formation

The simplicial type is declared as a set within the context Γ without any premises.

Γ ⊢ Δ : Type

Introduction

A simplicial set of rank n with elements S and constraints R is formed from context Γ if simplices, equalities, face maps, and degeneracy maps are properly defined.

Γ ⊢ n (S | R) : Simplicial if
Γ = s₀₁, …, sₙₘₙ : Simplex, r₁, …, rₚ ∧
    S₀, S₁, …, Sₙ = (s₀₁, …, s₀ₘ₀), …, (sₙ₁, …, sₙₘₙ) ∧
    rⱼ = tⱼ = tⱼ',
Γ ⊢ rⱼ : tⱼ = tⱼ' ∧
    ∂ᵢⱼ < sₖₗ,
Γ ⊢ ∂ᵢⱼ : sₖₗ → sₖ₋₁,ₘ ∧
    σᵢⱼ < sₖₗ,
Γ ⊢ σᵢⱼ : sₖₗ → sₖ₊₁,ₘ

Elim Face

The face map ∂ᵢⱼ extracts a simplex from s in a simplicial set if the constraint r defines the face relation.

Γ ⊢ ∂ᵢⱼ s : Simplex if
Γ ⊢ n (S | R) : Simplicial ∧
    r = ∂ᵢⱼ < s ∧
    r ∈ R ∧
    s ∈ S                                  

Elim Composition

The composition s₁ ∘ s₂ yields a simplex c in a simplicial set if the constraint r defines it and s1 and s2 are composable.

Γ ⊢ c : Simplex if
Γ ⊢ n (S | R) : Simplicial ∧
    r = c = s₁ ∘ s₂ ∧
    r ∈ R ∧ s₁, s₂ ∈ S ∧
Γ ⊢ ∂ᵢᵢ₋₁ s₁ = ∂ᵢ₀ s₂

Elim Degeneracy

The degeneracy map σᵢⱼ lifts a simplex s to a higher simplex in a simplicial set if the constraint r defines the degeneracy relation.

Γ ⊢ σᵢⱼ s : Simplex if
Γ ⊢ n (S | R) : Simplicial ∧
    r = σᵢⱼ < s,
    r ∈ R,
    s ∈ S

Face Computation

The face map ∂ᵢⱼ applied to a simplicial set reduces to the simplex s′ specified by the constraint r in R.

∂ᵢⱼ (n (S | R)) → s' if
    r = ∂ᵢⱼ < s' ∧
    r ∈ R ∧
    s' ∈ S

Composition Computation.

The composition s₁ ∘ s₂ applied to a simplicial set reduces to the simplex c specified by the constraint r in R, given s1 and s2 are composable.

(s₁ ∘ s₂) (n (S | R)) → c if
    r = c = s₁ ∘ s₂ ∧
    r ∈ R ∧
    s₁, s₂ ∈ S ∧
Γ ⊢ ∂ᵢᵢ₋₁ s₁ = ∂ᵢ₀ s₂

Degeneracy Computation.

The degeneracy map σᵢⱼ applied to a simplicial set reduces to the simplex s′ specified by the constraint r in R.

σᵢⱼ (n (S | R)) → s' if
    r = σᵢⱼ < s' ∧ 
    r ∈ R ∧ 
    s' ∈ S

Face Uniqueness

Two face maps ∂ᵢⱼ s and ∂ᵢⱼ s′ are equal if they are defined by constraints r and r′ across two simplicial sets with matching elements.

Γ ⊢ ∂ᵢⱼ s ≡ ∂ᵢⱼ s'  if  
Γ ⊢ n (S | R) : Simplicial ∧ 
    n (S' | R') : Simplicial ∧ 
    s ∈ S ∧ s' ∈ S' ∧ 
    r = ∂ᵢⱼ < s ∈ R ∧ 
    r' = ∂ᵢⱼ < s' ∈ R'

Uniqueness of Composition.

Two composed simplices c and c′ are equal if their constraints r and r′ define compositions of matching pairs s₁, s₂ and s₁′, s₂′ across two simplicial sets with composability conditions.

Γ ⊢ c ≡ c' if
Γ ⊢ n (S | R) : Simplicial ∧
    n (S' | R') : Simplicial ∧ 
    r = c = s₁ ∘ s₂ ∈ R ∧
    r' = c' = s₁' ∘ s₂' ∈ R' ∧
    s₁, s₂ ∈ S ∧ 
    s₁', s₂' ∈ S' ∧ 
Γ ⊢ ∂ᵢᵢ₋₁ s₁ = ∂ᵢ₀ s₂ ∧ 
Γ ⊢ ∂ᵢᵢ₋₁ s₁' = ∂ᵢ₀ s₂'

Uniqueness of Degeneracy.

Two degeneracy maps σᵢⱼ s and σᵢⱼ s′ are equal if they are defined by constraints r and r′ across two simplicial sets with matching elements.

Γ ⊢ σᵢⱼ s ≡ σᵢⱼ s' if
Γ ⊢ n (S | R) : Simplicial ∧
    n (S' | R') : Simplicial ∧
    s ∈ S ∧
    s' ∈ S' ∧
    r = σᵢⱼ < s ∈ R ∧
    r' = σᵢⱼ < s' ∈ R'

Examples

N-Monoid

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

O(5).

Category with Group (Path Category with Z/2Z)

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)

O(8)—5 context + 2 nested group + 1 constraint—linear with nesting.

Triangle Chain

def triangle_chain : Chain
 := П (v₀ v₁ v₂ e₀₁ e₀₂ e₁₂ t : Simplex),
      ∂₁₀ = e₀₁, ∂₁₁ = e₀₂, ∂₁₂ = e₁₂, ∂₂ < e₀₁ e₀₂ e₁₂
    ⊢ 2 (v₀ v₁ v₂, e₀₁ e₀₂ e₁₂, t | ∂₁₀ ∂₁₁ ∂₁₂, ∂₂)

O(11).

Simplicial Circle

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

O(5).

Z/3Z

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

O(4).

Triangle

def triangle : Simplex := П (a b c : Simplex),
         (ab bc ca : Simplex), ac = ab ∘ bc
         ⊢ 2 (a b c | ab bc ca)

O(7).

Singular Cone

def singular_cone : Simplex
 := П (p q r s : Simplex),
      (qrs prs pqs : Simplex), pqr = pqs ∘ qrs
    ⊢ 3 (p q r s | qrs prs pqs pqr)

Context: p, q, r, s: Simplex (vertices), qrs, prs, pqs : Simplex (faces), pqr = pqs ∘ qrs.

Simplex: Dimension 3, 4 faces.

Möbius Piece

def Möbius : Simplex
 := П (a b c : Simplex),
      (bc ac : Simplex), ab = bc ∘ ac
    ⊢ 2 (a b c | bc ac ab)

Context: a, b, c : Simplex (vertices), bc, ac : Simplex (faces), ab = bc ∘ ac (relation).

Simplex: Dimension 2, 3 faces.

Degenerate Tetrahedron

def degen_tetra : Simplex
 := П (p q r s : Simplex, q = r),
      (qrs prs pqs : Simplex), pqr = pqs ∘ qrs
    ⊢ 3 (p q r s | qrs prs pqs pqr)

Context: p, q, r, s : Simplex, q = r (degeneracy), qrs, prs, pqs : Simplex, pqr = pqs ∘ qrs.

Simplex: Dimension 3, 4 faces—degeneracy implies a collapsed edge.

Non-Triviality: q = r flattens the structure algebraically, testing composition under equality.

Twisted Annulus

def twisted_annulus : Simplex
 := П (a b c d : Simplex),
      (bc ac bd : Simplex), ab = bc ∘ ac, cd = ac ∘ bd
    ⊢ 2 (a b c | bc ac ab), 2 (b c d | bc bd cd)

Context:

• Vertices: a, b, c, d.
• Faces: bc, ac, bd.
• Relations: ab = bc ∘ ac, cd = ac ∘ bd (twist via composition).

Simplices:

• (a b c | bc, ac, ab ): First triangle.
• (b c d | bc, bd, cd ): Second triangle, sharing bc.

Checking:

• Vertices: a, b, c, d ∈ Γ — O(4).
• Faces: bc, ac, ab (O(3)), bc, bd, cd (O(3)) — total O(6).
• Relations: ab = bc ∘ ac (O(1)), cd = ac ∘ bd (O(1)) — O(2).
• Total: O(12) — linear, fast.

Degenerate Triangle (Collapsed Edge)

def degen_triangle : Simplex
 := П (a b c : Simplex, b = c),
      (bc ac : Simplex), ab = bc ∘ ac
    ⊢ 2 (a b c | bc ac ab)

Context:

• Vertices: a, b, c, with b = c.
• Faces: bc, ac.
• Relation: ab = bc ∘ ac.

Simplex:

• (a b c | bc, ac, ab ) — 3 faces, despite degeneracy.

Checking:

• Vertices: a, b, c ∈ Γ, b = c — O(3).
• Faces: bc, ac, ab ∈ Γ — O(3).
• Relation: ab = bc ∘ ac — O(1).
• Total: O(7)—efficient, handles degeneracy cleanly.

Singular Prism (Degenerate Face)

def singular_prism : Simplex
 := П (p q r s t : Simplex),
      (qrs prs pqt : Simplex, qrs = qrs), pqr = pqt ∘ qrs
    ⊢ 3 (p q r s | qrs prs pqt pqr)

Context:

• Vertices: p, q, r, s, t.
• Faces: qrs, prs, pqt.
• Relations: qrs = qrs (degenerate identity), pqr = pqt ∘ qrs.

Simplex:

• (p q r s | qrs, prs, pqt, pqr ) — 4 faces, one degenerate.

Checking:

• Vertices: p, q, r, s ∈ Γ (t unused, valid) — O(4).
• Faces: qrs, prs, pqt, pqr ∈ Γ — O(4).
• Relations: qrs = qrs (O(1)), pqr = pqt ∘ qrs (O(1)) — O(2).
• Total: O(10) — linear, fast despite degeneracy.

S¹ as ∞-Groupoid

def s1_infty : Simplicial
 := П (v e : Simplex),
      ∂₁₀ = v, ∂₁₁ = v, s₀ < v,
      ∂₂₀ = e ∘ e, s₁₀ < ∂₂₀
    ⊢ ∞ (v, e, ∂₂₀ | ∂₁₀ ∂₁₁, s₀, ∂₂₀, s₁₀)

AST:

(* Infinite S¹ ∞-groupoid *)
let s1_infty = {
  name = "s1_infty";
  typ = Simplicial;
  context = [
    Decl (["v"; "e"], Simplex);  (* Base point and loop *)
    Equality ("∂₁₀", Id "v", Id "∂₁₀");
    Equality ("∂₁₁", Id "v", Id "∂₁₁");
    Equality ("s₀", Id "e", Id "s₀");
    Equality ("∂₂₀", Comp (Id "e", Id "e"), Id "∂₂₀");  (* 2-cell: e ∘ e *)
    Equality ("s₁₀", Id "∂₂₀", Id "s₁₀")  (* Degeneracy for 2-cell *)
  ];
  rank = Infinite;  (* Unbounded dimensions *)
  elements = ["v"; "e"; "∂₂₀"];  (* Finite truncation: 0-, 1-, 2-cells *)
  constraints = [
    Eq (Id "∂₁₀", Id "v");
    Eq (Id "∂₁₁", Id "v");
    Map ("s₀", ["v"]);
    Eq (Id "∂₂₀", Comp (Id "e", Id "e"));
    Map ("s₁₀", ["∂₂₀"])
  ]
}

∞-Category with cube fillers

def cube_infty : Category := П (a b c : Simplex),
       (f g h : Simplex), cube2 = g ∘ f, cube2 : Simplex,
       cube3 = cube2 ∘ f, cube3 : Simplex
       ⊢ ∞ (a b c | cube2 cube3)

Matrix Ring Spectrum

def matrix_ring_spectrum : Ring
 := П (a b s p : Simplex),
      a + b = s, a ⋅ b = p,
      a = [[1,2],[3,4]], b = [[0,1],[1,0]], s = [[1,3],[4,4]], p = [[2,1],[4,3]]
    ⊢ 4 (a b s p | a + b = s, a ⋅ b = p, a = [[1,2],[3,4]], b = [[0,1],[1,0]],
                   s = [[1,3],[4,4]], p = [[2,1],[4,3]])

HZ spectrum

def hz_spectrum : Ring
 := П (x y p : Simplex),
      x ⋅ y = p,
      x = 2, y = 3, p = 6
    ⊢ 3 (x y p | x ⋅ y = p, x = 2, y = 3, p = 6)

Poly Ring spectrum

def poly_ring_zx : Ring
 := П (f g s p : Simplex),
      f + g = s, f ⋅ g = p,
      f = x + 1, g = 2 ⋅ x, s = 3 ⋅ x + 1, p = 2 ⋅ x ⋅ x + 2 ⋅ x
    ⊢ 4 (f g s p | f + g = s, f ⋅ g = p, f = x + 1, g = 2 ⋅ x,
                   s = 3 ⋅ x + 1, p = 2 ⋅ x ⋅ x + 2 ⋅ x)

GF(2⁴) Finite Field

def gf16 : Field
 := П (x y s p d : Simplex),
      x + y = s, x ⋅ y = p, x / y = d,
      x = Z(2^4), y = Z(2^4)^2,
      s = Z(2^4) + Z(2^4)^2,
      p = Z(2^4)^3, d = Z(2^4)^14
    ⊢ 5 (x y s p d | x + y = s, x ⋅ y = p, x / y = d,
                     x = Z(2^4), y = Z(2^4)^2,
                     s = Z(2^4) + Z(2^4)^2,
                     p = Z(2^4)^3,
                     d = Z(2^4)^14)

GF(7) Prime Field

def gf7 : Field
 := П (x y s p d : Simplex),
      x + y = s, x ⋅ y = p, x / y = d,
      x = 2, y = 3, s = 5, p = 6, d = 3
    ⊢ 5 (x y s p d | x + y = s, x ⋅ y = p,
         x / y = d, x = 2, y = 3,
         s = 5, p = 6, d = 3)

Bibliography

• Daniel Kan. Abstract Homotopy I. 1955.
• Daniel Kan. Abstract Homotopy II. 1956.
• Daniel Kan. On c.s.s. Complexes. 1957.
• Daniel Kan. A Combinatorial Definition of Homotopy Groups. 1958.
• Daniel Kan, W. G. Dwyer. Adjoint functors. 1958.
• Daniel Kan, W. G. Dwyer. Simplicial Localizations of Categories. 1980.
• Graeme Segal. Classifying spaces and spectral sequences. 1968.
• Graeme Segal. Categories and cohomology theories. 1974.
• Graeme Segal, R. Bott. Loop groups and their classifying spaces. 1988.
• Charles Rezk. A model for the homotopy theory of homotopy theory. 2001.
• Charles Rezk. A cartesian presentation of weak n-categories". 2010.
• Charles Rezk, S. Schwede, B. Shipley. Simplicial structures on model categories and functors. 2001.
• Charles Rezk, J. Bergner. Comparison of models for (∞,n)-categories. 2013.

Conclusion

Dan Kan Simplicity HoTT, hosted at groupoid/dan, is a lightweight, pure type checker built on Cubical Homotopy Type Theory (CCHM), named in tribute to Daniel Kan for his foundational work on simplicial sets. With a unified syntax — П (context) ⊢ n (elements | constraints) — Dan supports a rich type system Simplex, Group, Simplicial, Chain, Category, Monoid, now extended with ∞-categories featuring cube fillers.