gistfile1.txt

Let's build a Simplicial HoTT extension to CCHM/CHM/HTS type systems targeting GAP replacement, infinity-gategorical framework like Rezk prover (Riehl, Shulman) for Simplex and Simplicial types built into type checker. Then gradually extent type inference rules for Group, Monoid, Category, Chain, Ring, Field. As eliminators I propose Face, Degeneracies, Composition, as Introduction inference rule I propose Simplicial Object with common syntax:

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

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)

Consider examples:

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

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

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

Test this set of type system to ability of checking all existing theorems of all existing mathematics yet.

Create Very large cardinals extension Cardinal Type Theory