[FOM] New umbrella?

[Urs Schreiber]

This is an important point:

On 10/31/14, Freek Wiedijk <freek at cs.ru.nl> wrote:

>>The question is whether HoTT offers advantages in the
>>formalization of these theorems.
>
> I you want to use Coq?  Sure!  You get proper quotient
> types (= the set of equivalence classes under an equivalence
> relation), you get functional extensionality, you get "squash
> types" and therefore working in a proof irrelevant manner
> becomes much easier, etc. etc.  Lots of goodies that in Coq
> you need axioms for.  But axioms are frowned upon in the Coq
> community _apart from_ the HoTT axioms.  So if you want Coq,
> and you don't want all these irritating restrictions on
> what you get without being frowned upon, then HoTT's the way!
>
> However, if you want to work truly classically, and don't
> care about Coq idiosyncrasies, I'm not convinced.  In HoTT
> you _still_ don't get carefree classical mathematics.
> It still remains a very (maybe even more) complicated story
> of what you can do and what you can't do.


This is a very important point. Indeed this is essentially the very
point that I keep making regarding the point of HoTT. Let's get this
straight:

the reason that in Coq (in type theory) and in HoTT some of the
classical axioms are not imposed by default (but you may add them if
you wish), and hence the reason that it is not as "carefree" as
classical mathematics, as Freek says, is precisely what gives it the
power that makes people care about it. Because without these axioms,
whatever one proves in Coq is a much more general result than what it
would be with these axioms imposed. It is because of this very fact
that the short proof of Blakers-Massey in HoTT is automatically vastly
more general than the classical result of Blakers-Massey.

Because, without these classical axioms, whatever is proven in the
0-truncation of HoTT to h-sets is a statement not just about sets, but
about sheaves of sets on any site, which is an immensely richer
context. And whatever is proven in HoTT without restriction to h-sets
is a statement not just about bare homotopy types, but about sheaves
of homotopy types on any site (on any "infinity-site" even). This is
the power of HoTT that I tried to highlight when this discussion here
started.

If you wanted to rebuild sheaves of homotopy types in classical theory
it would be a huge and (I still think) practically intractable
undertaking. But the constructive logic of HoTT allows to reason about
them directly ("internally").

For that to work one has, as Freek amplifies above, exercise some care
and stick to the rules of constructive type theory, stick to its
"ideosyncracies" if you wish. While that is a little bit of effort, it
comes with an immense payoff that easily makes the effort worth it.

Finally, I think anyone interested in the concept of foundations will
appreciate the relevance of removing axioms and seeing how much may
still be proven. Since any system with fewer axioms may still be
enriched with these a posteriori, a system with fewer axioms is "more
foundational" than a system with more axioms, in an obvious sense.

That's how it works with HoTT: plain HoTT is the very foundational
theory of all infinity-toposes. As you add axioms, you may restrict it
to, for instance, just ordinary toposes (by imposing 0-truncation)
then you may further restrict to just the topos of sets (by imposing
choice and LEM etc.). That leaves you however in a tiny corner of the
vast universe that full HoTT is the theory of. You may tediously
rebuild that universe inside that tiny corner by building models of
infinity-toposes in set theory, but this will be immensely tedious and
is unlikely to be of practical use. Most importantly, it is
unnecessary. Instead, you may just remove those extra axioms again,
escape from the tiny corner of classical mathematics, and reason in
the foundational generality of full HoTT.