# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

martin-loef_type_theory [2014/11/10 20:32] nikolaj |
martin-loef_type_theory [2015/04/01 10:37] nikolaj |
||
---|---|---|---|

Line 1: | Line 1: | ||

===== Martin-Löf type theory ===== | ===== Martin-Löf type theory ===== | ||

- | ==== Meta ==== | + | ==== 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]] |