[FOM] formal proofs

Freek Wiedijk freek at cs.ru.nl
Thu Oct 23 06:21:22 EDT 2014


Dear Tim,

>This is a nice gauntlet!  Before a traditionalist embarks on a
>project to refute this claim, let me clarify what is at stake.
>
>Question for Urs: Suppose a traditionalist were to thoroughly refute
>your claim above.  Would that "score any points" for the traditional
>side in this debate?  Or is this just a casual remark on your part,
>which if refuted would not cause you to change your mind on any
>substantive issue?

I would guess that if one really would do this, still the
HoTT formalization would be much shorter.  So I think it
still would be taken as a reason to claim HoTT is much
better than the traditional way of working.

So one would really need to separate the formalization into
two parts: one part in which one formalizes the lemmas and
proof principles that in HoTT one gets for free.  And then
a second _very separate_ part, which would be a proof of
this Blakers-Massey theorem.  To make it a fair comparison.

Another question for Urs: if I were to formalize a model
of HoTT (cubical sets, is that a model for HoTT?) in a
traditional framework, and then just glue the Agda proof on
top of that, would that count as a refutation of the claim?

Also, I would like to understand the models of HoTT better.
If I just interpret the types as topological spaces and the
equalities as the existence of paths, do I get a model of
HoTT?  If not, why the the claim that HoTT is about homotopy
theory?  But if so, why all the fuzz about the cubical sets?

Freek


More information about the FOM mailing list