[FOM] New umbrella?

[Freek Wiedijk]

Dear Tim,

>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.

On the other hand Coq is much more expressive for abstract
mathematics (abstract algebra, category theory, etc.) than
the HOLs, and Coq and the HOLs seem the two best approaches
for actual practical formalization that we have right now.
It seems.  So maybe Coq+HoTT is the best we can do right now?
I don't know.

>For example, if HoTT had been around 15 years ago,
>would Hales have been much better off using HoTT for
>Flyspeck?

I wouldn't think so!  Flyspeck is about rather concrete
mathematics (volumes of subsets of 3-space, inequalities
between real expressions, etc.) and for that HOL works
perfectly well.

Freek