This is completely missing a core point of category theory and type theory (which is about categories equipped with certain extra structure), which is to work is settings which can be flexibly tightened or loosened in order to do constructions which are as general as possible. A theorem in HoTT is far more widely applicable than a theorem in ZFC; HoTT can be interpreted in any higher Gröthendieck topos, ZFC can be only intepreted in a certain class of 1-toposes. In HoTT, we can simply assume choice and LEM to internally reproduce ZFC. In ZFC, univalence is false and cannot be assumed.

> It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics

Xena project isn't too hot on HoTT indeed, but they will tell you that type theory in general is absolutely the best solution for formalizing mathematics.

> in particular denying the law of excluded middle

MLTT does not deny LEM, nor HoTT. The point is not to deny LEM, but to work in a more general system which does not necessarily assume it.

id(X): ==(X, rec_0(0, X))

Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.

In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.

We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.

> The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem

Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.

The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type checking, as I explained before.

ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness.

It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking.

For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.

Decidability of type checking is instead related to how explicit surface syntax is. In intensional type theory, the usage of equality proofs is marked explicitly, which is sufficient to retain decidable type checking. In contrast, in extensional type theory, the usage of equality proofs is left implicit, which causes type checking to be undecidable.

https://web.archive.org/web/20200518081726/https://slatestar...

http://okmij.org/ftp/ML/generalization.html

https://www.nickbostrom.com/fut/evolution.html

In programming, this is more commonly available, because we don't necessarily care about propositions, let alone classical logical proofs. The polymorphic identity function type `forall a. a -> a` in System F quantifies over all types including itself.

It is fair to say that functional programming is primrarily in favor of immutable data structures because it is simpler to implement them efficiently in a setting where referential transparency is the default. Mutation (meaning referential intrasparency) is just more complicated, and we need heavier machinery to structure it nicely. We may use linear/substructural types, uniqueness types, regions, etc for this purpose, but here are a number of choices, and the picture is not as clear-cut as with plain pure lambda calculi. Just remember that mutation is not bad by itself, many functional programmers are often happy to speed up production code with mutation, it's just that it is usually more complicated to structure nicely.

The ST-like region typing can be still useful though, because we get a static bound on the lifetime of a compact region. We'd prefer to avoid leaking space via large compact regions which survive beyond their intended life.