[FOM] Concerning Univalent Universes

[Harvey Friedman]

McLarty wrote:

Kapulkin, Lumsdaine, and Voevodsky (mathematics arXiv, 1211.2851v2)
use ZFC plus two Grothendieck universes to prove consistency of a
Univalent Universe in Martin-Löf Type Theory.  They even show that if
the Universe is to be defined by a cardinal bound on the sets, then
that bound must be a strong inaccessible.

I have just posted http://arxiv.org/abs/1412.6714 showing that the use
of a definability bound instead of cardinality allows essentially the
same model construction to work at the consistency strength of finite
order arithmetic.
...

For the ASL next week I expect to present a proof that I am now
checking, to show Zermelo set theory plus existence of a standard
model of Zermelo set theory suffices to prove consistency of a
Univalent universe with full Martin-Löf type theory -- though I am not
yet clear what would make an equiconsistency result for this case.

*******************

Some time ago, on the FOM I raised the question of just what work
univalent universes or univalent foundational ideas are doing that
can't be done as well or better by standard f.o.m. through ZF(C) and
standard variants such as NBG and perhaps extensions via large
cardinal hypotheses. I indicated some initial steps in this direction.
I didn't get much of a dialog going from strong advocates like Awodey
and others.

Colin McLarty looks to be an excellent candidate for participating in
such a discussion now.

To set the stage, the foundational work in question that is proposed
to be better done with univalent ideas than standard f.o.m. ideas
cannot be the longstanding major classical issues. In particular,

*) does highly abstract (i.e., highly above the computational) have
any substantial or essential use for highly concrete (i.e., at or near
the computational) fundamental mathematics?

The relevant point to be emphasized is that at the highly concrete
level, there are no substantive issues of formulation of the
mathematics. At the highly abstract level, there are different views
as to what makes sense and is natural. E.g., the general notion of set
is not something that many mathematicians are really comfortable with.
SImilarly, any general notion of category, natural transformation,
topos, etcetera, is equally uncomfortable for others. Finite sets of
integers/rationals is of course not a problem for anyone.

Furthermore, playing around at the abstract level results in mutual
interpretability and conservative extensions for concrete statements.

At the moment, there is absolutely no comparison between the insight
gained with the usual f.o.m. approach to *)., as opposed to other
approaches The whole of large cardinal theory is very naturally
addressed in the usual f.o.m. framework.

So far, all that I see from univalentists is a general claim that

**) if you want to actually formalize actual mathematics, at least in
some areas of highly abstract mathematics, then you should (must) use
univalent ideas and cannot proceed in any appropriate way with
standard f.o.m. ideas.

Two comments.

1. **) deals with a matter whose significance is, prima facie, minor
compared to *). The overwhelming view of the mathematics community is
that there is no genuine need for formalizing proofs. Furthermore,
that for the foreseeable future there is absolutely no prospect of
this being worth the enormous effort for the really important deep
mathematical proofs.

2. My own view is more nuanced, and I am quite interested in whether
and how formal verification can be made far more friendly than it is
now. I am also interested in understanding general features of
formalized proofs - as a kind of applied proof theory. However, I
doubt very much if developing apparently ad hoc methods to handle
certain kinds of highly abstract mathematics is anything like the way
to go to attack this on a GENERAL PURPOSE level. The long term project
of developing a huge variety of massively powerful decision procedures
for fragments of undecidable theories is vastly more promising - and
of incomparably higher general intellectual interest.

3. SO I THINK THAT many FOM readers, including me, would be quite
interested in getting Colin involved in a discussion of this.

Harvey Friedman