4 ms·
Martin-Lof's type theory is the foundation (or inspiration) for quite a few modern proof assistants. It is also an elegant non-set based foundation for construc
by deterministic 1y ago
Martin-Lof's type theory is the foundation (or inspiration) for quite a few modern proof assistants. It is also an elegant non-set based foundation for constructive mathematics.
- wduquette 1y agoAnd there it is. Thanks very much!