3 ms·
Yeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to di
by tel 13y ago
Yeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to distinguish MLTT from just type theory since plain-old-TT might be harder to distinguish as something interesting above `(int *)`.
But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.
- mafribe 13y agoPer Martin-Löf was instrumental in extending type theory to dependent types, although the first version of his dependent type theory was impredicative with Type:Type and was shown to be inconsistent by J.-Y. Girard. Subsequent versions of Martin-Löf type theory have been predicative, but other dependent type theories (such as the calculus of constructions) stuck with (more benign forms of) impredicativity.