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)

Let's build a language that can mechanically verify any existed mathematics (theorems). I propose following core:

1. Dan Kan Simplicial HoTT. It supports following core type built into type checker: Chain, Cochain, Simplex, Simplicial, Category, Monoid, Group, Ring and can manipulate directly with ∞-categories with Rezk, Segal Kan simplicial modes. Γ ⊢ 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ₖ₊₁,ₘ.
2. Jack Morava Type Theory. It supports following core type built into type checker HopfFibrationⁿ (n=1,2,3,4), Susp(A), Truncⁿ(A), ℕ, ℕ∞, Π(x:A).B, Σ(x:A).B, Id_A(u, v), Spec, πₙ^S(A), S⁰[p], Group, A ∧ B, [A, B], Hⁿ(X; G), G ⊗ H, SS(E, r). Intro: x, 𝟎, suc(t), fin(t), inf, hopfⁿ, susp(t), truncⁿ(t), λx.t, t u, (t, u), fst(t), snd(t), p, refl, spec({Aₙ},{σₙ}),.
3. Equivariant Super Type Theory based on Cohesite Type Theory: ⊢ Uᵢ^|0| : Uᵢ₊₁^|0|, ⊢ Uᵢ^|1| : Uᵢ₊₁^|0|.

• Graded Tensor: Γ ⊢ A : Uᵢ^g₁, Γ ⊢ B : Uᵢ^g₂ → Γ ⊢ A ⊗ B : Uᵢ^(g₁ + g₂) Γ ⊢ a : A, Γ ⊢ b : B → Γ ⊢ a ⊗ b : A ⊗ B Γ ⊢ a : A^g₁, Γ ⊢ b : B^g₂ → Γ ⊢ a ⊗ b = (−1)^(g₁ g₂) b ⊗ a : A ⊗ B.
• Group Action: Γ, g : 𝔾 ⊢ A : Uᵢ^g → Γ ⊢ 𝔾 → A : Uᵢ^g.
• Super Type Theory: Uᵍᵢ| 𝖘 A | 𝔾 → A.
• Super Modality: Γ ⊢ A : Uᵢ^g → Γ ⊢ 𝖘 A : Uᵢ^g.
• Cohesive Type Theory: ∣ ʃ ∣ ♭ ∣ ♯ ∣ ℑ | & | ℜ .
  Γ ⊢ A : Uᵢ → Γ ⊢ |ʃ A : Uᵢ // Shape modality (homotopy type) Γ ⊢ A : Uᵢ → Γ ⊢ |♭ A : Uᵢ // Discrete flat modality (points) Γ ⊢ A : Uᵢ → Γ ⊢ |♯ A : Uᵢ // Sharp modality (codiscrete) Γ ⊢ A : Uᵢ → Γ ⊢ |ℑ A : Uᵢ // Infinitesimal shape (de Rham stack) Γ ⊢ A : Uᵢ → Γ ⊢ |& A : Uᵢ // Infinitesimal flat (infinitesimal points) Γ ⊢ A : Uᵢ → Γ ⊢ |ℜ A : Uᵢ // Coreduced infinitesimal flat (bemol)

Will that be sufficial?

Ok let's cover. It's not that much. Let's perform next steps:

1. Dedekind Real Type Theory.
2. ZFC specialized type theory with LEM extension.
3. Reduce modality redundancies.

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