===== Martin-Löf type theory =====
==== Framework ====
A [[Dependent type theory]] with [[Identity type]]. Or rather it's an umbrella term for several closely related such theories.

-----
=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Intuitionistic_type_theory|Intuitionistic type theory]]

-----
=== Requirements ===
[[Identity type]]