Embed Notice

Martin-Löf type theory (MLTT) is a minimal foundation for mathematics, which is at the same time a programming language.

(E.g. Agda is based on MLTT.)

Compared to classical (non-constructive) mathematics, it lacks the principle of excluded middle.

Compared to Brouwer's intuitionism, it lacks continuity and bar-induction principles.

Compared to (the internal language of) topos theory, it lacks impredicativity and has a different treatment of the existential quantifier.

Compared to Homotopy Type Theory (HoTT), it lacks the univalence axiom and higher-inductive types.

The above mathematical theories can be accommodated in MLTT by simply postulating the required "missing" axioms (excluded middle, choice, propositional resizing, propositional truncations, univalence etc.)

2/