On Tuesday, 5 June 2018 09:37:41 UTC+1, David Roberts wrote:There is an... "interesting" discussion going on at the fom mailing
list at present, the usual suspects included, about set theory-based
proof assistants, which might provide either a source of entertainment
or frustration. It is enlightening when considering what people think
about typed vs untyped.
Univalent foundations gets a mention here:
https://cs.nyu.edu/pipermail/fom/2018-May/021012.html
The 'ideal proof assistant' is described as being based on ZFC here:
https://cs.nyu.edu/pipermail/fom/2018-May/021026.html
Friedman proclaims he is completely ignorant of the issues and that he
has never gotten close to getting dirty with details, but is happy to
weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html
The discussion continues this month here:
https://cs.nyu.edu/pipermail/fom/2018-June/021030.html
May I humbly say that the FOM list is mainly concerned with the foundations of mathematics of hlevel 2, or 0-types.
And that they are concerned with "how much" a foundation can prove, rather than "what" a foundation talks about *natively*? (As opposed to via ZFC-set avatars.)
What univalent mathematics proposes is that infty-groupoids are the primitive objects of mathematics, rather than ZFC sets (imprecisely mirrored by 1-groupoids).
We call these things types (bad terminology, inherited from history).
From this point of view, the above FOM discussion is completely misguided. (As you already know.)
The point of univalent foundations is that we should be able to talk about the objects we have in mind directly as they are, rather than via ZFC avatars.
It is not that we worship types.
Martin