Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
martin-loef_type_theory [2014/11/10 18:09] nikolaj |
martin-loef_type_theory [2014/11/10 20:30] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Martin-Löf type theory ===== | ===== Martin-Löf type theory ===== | ||
| ==== Meta ==== | ==== Meta ==== | ||
| - | >todo | + | A [[Dependent type theory]] with [[Identity type]]. Or rather it's an umbrella term for several closely related such theories. |
| ==== Discussion ==== | ==== Discussion ==== | ||
| - | >todo | ||
| === Reference === | === Reference === | ||
| - | >todo | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Requirements === | === Requirements === | ||
| [[Dependent type theory]], [[Identity type]] | [[Dependent type theory]], [[Identity type]] | ||
