[[!redirects Martin-Löf Intensional Type Theory]] A [[type theory]] created by [[Per Martin-Löf]] in 1972. Martin-Löf created both intensional and extensional variants.