ttSystem
plain-language theorem explainer
Martin-Löf type theory is packaged as a formal system whose tokens are the two closed terms of the Boolean type, discrimination is term inequality, and expression order is derivation-length order. Anyone citing that type theory realizes the δ core or is non-degenerate uses this parse. The body is a direct structure instance filling each field of the minimal formal-system interface.
Claim. The MLTT parse is the formal system with token type the two-element type $2$ (closed terms $\mathsf{false}$, $\mathsf{true}$), expressions $\mathbb{N}$ ordered by $\le$, discrimination given by inequality of tokens, and endpoint map sending the left (resp. right) side of a primitive distinction to $\mathsf{false}$ (resp. $\mathsf{true}$). Finite recognition traces are read as expressions via trace length.
background
The Primitive Recognition Calculus isolates a minimal formal-system interface for the inevitability theorem: carriers for tokens and expressions, a discrimination relation on tokens, an extension preorder on expressions, a map from distinction endpoints to tokens, and a reading of finite recognition traces as expressions that is monotone under extension.
Tokens here are the canonical two-element type of MLTT (Lean Bool), with closed terms false and true. Side labels the two sides forced by a primitive distinction. A Trace is empty or extended by one distinction act; its length counts those acts. The upstream fact length_le_of_extends states that finite-trace length is monotone under trace extension.
This module supplies the type-theory parse of that interface so MLTT can be compared with the δ core and the distinction dichotomy alongside the set-theory and category-theory parses.
proof idea
Direct structure instance, not a derived theorem. Token is the two-element type; Expr is $\mathbb{N}$; distinguishes is propositional inequality; exprExtends is $\le$ on naturals. The endpoint map pattern-matches on Side, sending left to false and right to true. Traces are read by Trace.length, and the monotonicity field is discharged by applying length_le_of_extends.
why it matters
This is the type-theory leg of the three-foundations package. Downstream, ttSystem_expressive shows the two tokens are distinct, ttSystem_embeds_delta concludes MLTT contains the δ core ("MLTT contains the δ core"), and ttSystem_not_degenerate places it on the non-degenerate side of the distinction dichotomy. Those facts feed three_foundations_realize_delta and three_foundations_not_degenerate, which assert that set theory, type theory, and category theory each realize δ and none is degenerate. In the Recognition foundation layer this shows MLTT already carries the primitive recognition structure rather than sitting outside it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.