[[!redirects Martin-Löf Type Theory]] [[!redirects Martin-Löf Intensional Type Theory]] < [[nlab:Martin-Löf dependent type theory]]