Homotopy Type Theory
Martin-Löf Type Theory

A type theory created by Per Martin-Löf in 1972. Martin-Löf created both intensional and extensional variants.