("Imprecisely mirrored by 0-groupoids" - apologies for the typo.)

On Tuesday, 5 June 2018 23:19:20 UTC+1, Martín Hötzel Escardó wrote:
>
>
>
> 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
>
>