Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
martin-loef_type_theory [2014/11/11 11:12] nikolaj |
martin-loef_type_theory [2015/04/01 10:37] nikolaj |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| ==== Framework ==== | ==== Framework ==== | ||
| A [[Dependent type theory]] with [[Identity type]]. Or rather it's an umbrella term for several closely related such theories. | A [[Dependent type theory]] with [[Identity type]]. Or rather it's an umbrella term for several closely related such theories. | ||
| - | ==== Discussion ==== | + | |
| + | ----- | ||
| === Reference === | === Reference === | ||
| Wikipedia: [[http://en.wikipedia.org/wiki/Intuitionistic_type_theory|Intuitionistic type theory]] | Wikipedia: [[http://en.wikipedia.org/wiki/Intuitionistic_type_theory|Intuitionistic type theory]] | ||
| - | ==== Parents ==== | + | |
| + | ----- | ||
| === Requirements === | === Requirements === | ||
| [[Identity type]] | [[Identity type]] | ||
