[[!redirects Martin-Loef type theory]] [[!redirects intensional Martin-Loef type theory]] < [[nlab:Martin-Löf dependent type theory]]