Martin-Löf Type Theory (MLTT)
Overview
Martin-Löf Type Theory (MLTT): dependent type theory as a foundation for constructive mathematics and proof assistants. Judgments Γ ⊢ t : T; dependent products Π and sums Σ; identity types; inductive types (ℕ, W-types) with elimination (recursion). Propositions as types; proofs as terms (Curry–Howard). Predates HoTT; HoTT extends MLTT with homotopy interpretation and optionally univalence.
Era: 1971–1984
Proposed at: Stockholm, Sweden
Formal structure
Domain: Context Γ; types A, B; terms t; judgments Γ ⊢ t : T
Π(x:A).B(x), Σ(x:A).B(x), Id_A(a,b); ℕ-elim / dependent elimination
Constraints: Constructive: intuitionistic logic; no unrestricted excluded middle
Objective: Formalize mathematics; extract programs from proofs; basis for Agda, Coq, Lean core