[FOM] Wiki: type theoretic fnds

[Harvey Friedman]

I looked some at

https://en.wikipedia.org/wiki/Univalent_foundations

https://en.wikipedia.org/wiki/Homotopy_type_theory

As I expected, I could not find a single example of any of the following:

1. Some issue in f.o.m. that is not being addressed by the usual f.o.m.
2. Some issue in f.o.m. that is being addressed by type theoretic f.o.m.

I see some new algebraic/topological type interpretations of type
theories, and the like.

Although it wasn't clear from these articles, I could imagine that
there is some kinds of type theories for which it is not at all
obvious that one has any mathematical model, or even that one has any
model at all in any reasonable sense.

So the impression one inevitably gets is that this stuff is

a. A framework for doing some new kinds of abstract categorical
algebra/topology that is exciting to very abstractly minded
mathematicians.
b. A complicated solution in search of a foundational problem.

So I repeat my suspicion and therefore my challenge.

Anything that can be done with this kind of "foundations" can be done
much more simply and much more powerfully and much more effectively by
sugaring the usual f.o.m.

But I can't start backing this up, and others cannot really challenge
me, until they state a crystal clear foundational issue that they
think is not or cannot be addressed in standard f.o.m., and that is
addressed in this exotic f.o.m.

One thing that does not seem to be in doubt, correct me if I am wrong.
This exotic f.o.m. is much more complicated than standard f.o.m.

Perhaps we should start with a simpler question.

What foundational issue is addressed by even ML type theory - no
univalence axiom - that cannot be more simply and better addressed by
standard f.o.m.?

Let me close with a methodological question.

What standards should be applied by proposing to replace an existing
system with another system that is massively more complicated?

My answer of course as you see, is to ask for careful generally
understandable explanations as to what is to be gained. There also
needs to be a major effort made to see if the existing much simpler
system already can be used to address the issues, whatever they are,
adequately, or maybe even better.

Harvey Friedman