[FOM] formal proofs

[Freek Wiedijk]

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