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)

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)

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)

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)

The type checker AST Types:

type superscript = S1 | S2 | S3 | S4 | S5 | S6 | S7 | S8 | S9
type type_name = Simplex | Group | Simplicial | Chain | Category | Monoid | Ring | Field

type term =
| Id of string
| Comp of term * term
| Inv of term
| Pow of term * superscript
| E
| Matrix of int list list
| Add of term * term (* r₁ + r₂ )
| Mul of term * term ( r₁ ⋅ r₂ )
| Div of term * term ( r₁ / r₂ *)

type constrain =
| Eq of term * term
| Map of string * string list

type hypothesis =
| Decl of string list * type_name (* e.g., (a b c : Simplex) )
| Equality of string * term * term ( e.g., ac = ab ∘ bc )
| Mapping of string * term * term ( e.g., ∂₁ = C₂ < C₃ *)

type rank = Finite of int | Infinite (* Updated to support ∞ *)

type type_def = {
name : string;
typ : type_name;
context : hypothesis list;
rank : rank; (* )
elements : string list; ( )
faces : string list option; ( Optional: only for Simplex )
constraints : constrain list ( *)
}

(* Parsing helpers *)
let parse_superscript = function
| "¹" -> S1 | "²" -> S2 | "³" -> S3 | "⁴" -> S4 | "⁵" -> S5
| "⁶" -> S6 | "⁷" -> S7 | "⁸" -> S8 | "⁹" -> S9 | _ -> failwith "Invalid superscript"

let parse_n s = match s with
| "∞" -> Infinite
| n -> Finite (int_of_string n)

Example:

let mobius = {
name = "Möbius";
typ = Simplex;
context = [
Decl (["a"; "b"; "c"], Simplex);
Decl (["ab"; "bc"; "ac"], Simplex);
Equality ("ab", Comp (Id "bc", Id "ac"), Id "ab")
];
rank = Finite 2;
elements = ["a"; "b"; "c"];
faces = Some ["bc"; "ac"; "ab"];
constraints = [Eq (Id "ab", Comp (Id "bc", Id "ac"))]
}

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