Почему мне нравится MLTT в качестве оснований математики

Почему мне нравится MLTT в качестве оснований математики: полностью описано в десятилетней давности статье Ратьена “The constructive Hilbert program and the limits of Martin-Löf type theory”, http://hlombardi.free.fr/Rathjen-ConstructiveHilbertProgram.pdf

С концептуальной точки зрения MLTT пример совершенства: Logic Free Theory с рефлексией, с удивительным свойством что с одной стороны утвреждения и доказательства сами являются объектами теории, с другой стороны теория имеет вычислительное содержание совпадающее с realizability interpretation. Ну и ко всему это ещё и classicality-agnostic theory, можно заниматься интуиционистской математикой и работать в подсистеме арифметики второго порядка, можно принять постулат исключённого третьего и работать в арифметике второго порядка per se, можно принять аксиому выбора и работать в консервативной надсистеме ZFC.

Из конкурентов, обладающих какими-то уникальными концептуальными свойствами, (пока) не разделяемыми MLTT имеются только
– Фефермановская Explicit mathematics, имеющая очень здравый подход к частично-вычислимым функциям;
– Жираровская Ludics, у которой синтаксис сам себе семантика.