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