ID	c1a0c605-806c-4510-8853-ea9a48619a21
DeertopiaVisibility	public
ROAM_ALIASES	MLTT

Martin-Löf type theory

Martin-Löf type theory (MLTT) is a predicative type theory and alternative foundation of mathematics using dependent types.

Implementation

There are several different implementations and variants of MLTT, several of which are Martin-Löf's own. Concrete implementations include Epigram, Agda, and Idris.

Nonetheless, one possible description of MLTT is given here.

\begin{matrix} \begin{matrix} e, τ & : : = & x & Variable \\ | & e e & Application \\ | & \Typen u & Universe \\ | & λ Type x τ . e & λ -abstraction \\ | & \pitype Type x τ e & Dependent function space \end{matrix} \end{matrix}

\begin{matrix} \inference \rules Γ \Typen u : \Typen u + 1 [Univ] \\ \inference \rules Γ Type τ \Typen u \rules Γ, Type x τ Type x τ [Var] \\ \inference \rules Γ Type σ \Typen u \inferencesep \rules Γ, Type x σ m : τ \rules Γ Type (λ Type x σ . m) \pitype Type x σ τ [Lam] \\ \inference \rules Γ Type σ \Typen u \inferencesep \rules Γ, Type x σ Type τ \Typen v \rules Γ Type (\pitype Type x σ τ) \Typen \max (u, v) [Pi] \\ \inference \rules Γ Type f (\pitype Type x σ τ) \inferencesep \rules Γ Type y σ \rules Γ Type f y subst τ x y [App] \end{matrix}