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.

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 (v0, ..., vk | f0, ..., fl | ... ) 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.

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

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

New sequent contruction:

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

Instances:

def chain : Chain := П (context), conditions ⊢ n (C0, C1, ..., Cn | ∂0, ∂1, ..., ∂n−1)
def simplicial : Simplicial := П (context), conditions ⊢ n (s0, s1, ..., sn | facemaps, degeneracies)
def group : Group := П (context), conditions ⊢ n (generators | relations)
def cat : Category := П (context), conditions ⊢ n (objects | morphisms | coherence)

<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> ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<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., ∂1 = C2 < C3
 | <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., ∂1 < C2
<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., a3
 | "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).

• Formation. Γ ⊢ Chain : Set
• Intro. Γ ⊢ n (S | R) : Chain if Γ = s01, ..., snmn : Simplex, r1, ..., rp ∧ S0, S1, ..., Sn = (s01, ..., s0m0), ..., (sn1, ..., snmn) ∧ ∀ rj = tj = tj', Γ ⊢ rj : tj = tj' ∧ ∀ ∂ij < skl, Γ ⊢ ∂ij : skl → sk−1,m
• Elim Face. Γ ⊢ ∂ij s : Simplex if Γ ⊢ n (S | R) : Chain ∧ r = ∂ij < s ∧ r ∈ R ∧ s ∈ S
• Comp Face. ∂ij (n (S | R)) → s' if r = ∂ij < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Face. Γ ⊢ ∂ij s ≡ ∂ij s' if Γ ⊢ n (S | R) : Chain ∧ n (S' | R') : Chain ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = ∂ij < s ∈ R ∧ r' = ∂ij < s' ∈ R'

• Formation. Γ ⊢ Cochain : Set
• Intro. Γ ⊢ n (S | R) : Cochain if Γ = s01, ..., snmn : Simplex, r1, ..., rp ∧ S0, S1, ..., Sn = (s01, ..., s0m0), ..., (sn1, ..., snmn) ∧ ∀ rj = tj = tj', Γ ⊢ rj : tj = tj' ∧ ∀ σij < skl, Γ ⊢ σij : skl → sk+1,m
• Elim Degeneracy. Γ ⊢ σij s : Simplex if Γ ⊢ n (S | R) : Cochain ∧ r = σij < s ∧ r ∈ R ∧ s ∈ S
• Comp Degeneracy. σij (n (S | R)) → s' if r = σij < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Degeneracy. Γ ⊢ σij s ≡ σij s' if Γ ⊢ n (S | R) : Cochain ∧ n (S' | R') : Cochain ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = σij < s ∈ R ∧ r' = σij < s' ∈ R'

• Formation. Γ ⊢ Category : Set
• Intro. Γ ⊢ n (O | M | R) : Category if Γ = o1, ..., on, m1, ..., mk : Simplex, r1, ..., rp ∧ O = (o1, ..., on) ∧ M = (m1, ..., mn) ∧ ∀ rj = tj = tj', Γ ⊢ rj : tj = tj' ∧ ∀ tj = ma ∘ mβ, ma, mβ ∈ Γ
• Elim Comp. Γ ⊢ c : Simplex if Γ ⊢ n (O | M | R) : Category ∧ r = c = m1 ∘ m2 ∧ r ∈ R ∧ m1, m2 ∈ Γ
• Comp Comp. (m1 ∘ m2) (n (O | M | R)) → c if r = c = m1 ∘ m2 ∧ r ∈ R ∧ m1, m2 ∈ Γ
• Uniq Comp. Γ ⊢ c ≡ c' if Γ ⊢ n (O | M | R) : Category ∧ n (O' | M' | R') : Category ∧ r = c = m1 ∘ m2 ∈ R ∧ r' = c' = m1' ∘ m2' ∈ R' ∧ m1, m2 ∈ Γ ∧ m1', m2' ∈ Γ'

• Formation. Γ ⊢ Monoid : Set
• Intro. Γ ⊢ n (M | R) : Monoid if Γ = m1, ..., mn : Simplex, r1, ..., rp ∧ M = (m1, ..., mn) ∧ ∀ rj = tj = tj', Γ ⊢ rj : tj = tj' ∧ ∀ tj = ma ∘ mβ, ma, mβ ∈ M
• Elim Comp. Γ ⊢ c : Simplex if Γ ⊢ n (M | R) : Monoid ∧ r = c = m1 ∘ m2 ∧ r ∈ R ∧ m1, m2 ∈ M
• Comp Comp. (m1 ∘ m2) (n (M | R)) → c if r = c = m1 ∘ m2 ∧ r ∈ R ∧ m1, m2 ∈ M
• Uniq Comp. Γ ⊢ c ≡ c' if Γ ⊢ n (M | R) : Monoid ∧ n (M' | R') : Monoid ∧ r = c = m1 ∘ m2 ∈ R ∧ r' = c' = m1' ∘ m2' ∈ R' ∧ m1, m2 ∈ M ∧ m1', m2' ∈ M'

• Formation. Γ ⊢ Simplex : Set
• Intro. Γ ⊢ n (S | R) : Simplex if Γ = s0, ..., sn : Simplex, r1, ..., rp ∧ |S| = n + 1 ∧ ∀ rj = tj = tj', Γ ⊢ rj : tj = tj' ∧ ∀ ∂i < sk, Γ ⊢ ∂i : sk → sk−1 ∧ ∀ σi < sk, Γ ⊢ σi : sk → sk+1
• Elim Face. Γ ⊢ ∂i s : Simplex if Γ ⊢ n (S | R) : Simplex ∧ r = ∂i < s ∧ r ∈ R ∧ s ∈ S
• Elim Degeneracy. Γ ⊢ σi s : Simplex if Γ ⊢ n (S | R) : Simplex ∧ r = σi < s ∧ r ∈ R ∧ s ∈ S
• Comp Face. ∂i (n (S | R)) → s' if r = ∂i < s' ∧ r ∈ R ∧ s' ∈ S
• Comp Degeneracy. σi (n (S | R)) → s' if r = σi < s' ∧ r ∈ R ∧ s' ∈ S
• Uniq Face. Γ ⊢ ∂i s ≡ ∂i s' if Γ ⊢ n (S | R) : Simplex ∧ n (S' | R') : Simplex ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = ∂i < s ∈ R ∧ r' = ∂i < s' ∈ R'
• Uniq Degeneracy. Γ ⊢ σi s ≡ σi s' if Γ ⊢ n (S | R) : Simplex ∧ n (S' | R') : Simplex ∧ s ∈ S ∧ s' ∈ S' ∧ ∀ r = σi < s ∈ R ∧ r' = σi < s' ∈ R'

• Γ ⊢ Δn : Type (Simplex)
• Γ ⊢ Δnkan : Type
• Γ ⊢ Δnrezk : Type
• Γ ⊢ Δnsegal : Type

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

Γ ⊢ Δ : Type

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
Γ = s01, ..., snmn : Simplex, r1, ..., rp ∧
 S0, S1, ..., Sn = (s01, ..., s0m0), ..., (sn1, ..., snmn) ∧
 rj = tj = tj',
Γ ⊢ rj : tj = tj' ∧
 ∂ij < skl,
Γ ⊢ ∂ij : skl → sk−1,m ∧
 σij < skl,
Γ ⊢ σij : skl → sk+1,m

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

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

The composition s1 ∘ s2 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 = s1 ∘ s2 ∧
 r ∈ R ∧ s1, s2 ∈ S ∧
Γ ⊢ ∂ii−1 s1 = ∂i0 s2

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

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

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

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

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

(s1 ∘ s2) (n (S | R)) → c if
 r = c = s1 ∘ s2 ∧
 r ∈ R ∧
 s1, s2 ∈ S ∧
Γ ⊢ ∂ii−1 s1 = ∂i0 s2

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

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

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

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

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

Γ ⊢ c ≡ c' if
Γ ⊢ n (S | R) : Simplicial ∧
 n (S' | R') : Simplicial ∧ 
 r = c = s1 ∘ s2 ∈ R ∧
 r' = c' = s1' ∘ s2' ∈ R' ∧
 s1, s2 ∈ S ∧ 
 s1', s2' ∈ S' ∧ 
Γ ⊢ ∂ii−1 s1 = ∂i0 s2 ∧ 
Γ ⊢ ∂ii−1 s1' = ∂i0 s2'

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

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

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

O(5).

def path_z2_category : Category
 := П (x y : Simplex),
 (f g h : Simplex),
 (z2 : Group(П (e a : Simplex), a2 = e ⊢ 1 (a | a2 = 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.

def triangle_chain : Chain
 := П (v0 v1 v2 e01 e02 e12 t : Simplex),
 ∂10 = e01, ∂11 = e02, ∂12 = e12, ∂2 < e01 e02 e12
 ⊢ 2 (v0 v1 v2, e01 e02 e12, t | ∂10 ∂11 ∂12, ∂2)

O(11).

def circle : Simplicial
 := П (v e : Simplex),
 ∂10 = v, ∂11 = v, s0 < v
 ⊢ 1 (v, e | ∂10 ∂11, s0)

O(5).

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

O(4).

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

O(7).

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.

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.

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.

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.

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.

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.

def s1_infty : Simplicial
 := П (v e : Simplex),
 ∂10 = v, ∂11 = v, s0 < v,
 ∂20 = e ∘ e, s10 < ∂20
 ⊢ ∞ (v, e, ∂20 | ∂10 ∂11, s0, ∂20, s10)

AST:

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

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)

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]])

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)

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)

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)

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)

• 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.

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.