[FOM] New Umbrella?

[Urs Schreiber]

On 10/29/14, Monroe Eskew <meskew at math.uci.edu> wrote:
>
>> On Oct 29, 2014, at 4:43 AM, Urs Schreiber <urs.schreiber at googlemail.com>
>> wrote:
>>
>> There is ongoing work is this direction, the most developed is
>> presently the approach of building models for HoTT in terms of cubical
>> sets in constructive set theory/type theory; by Bezem-Coquand-Huber
>> and by Kaproi-Altenkirch and others, see here:
>>
>> http://ncatlab.org/nlab/show/cubical+set#BezemCoquandHuber13
>> http://ncatlab.org/nlab/show/cubical+set#KaposiAltenkirch14

> This paper seems more like what I had in mind:
>
> http://arxiv.org/abs/1211.2851
>
> Since the mathematical work is already done, now we can formalize this as a
> machine-checkable proof in ZFC+2 inaccessibles, incorporating a definition
> of HoTT derivability in terms of the usual Gödel coding of syntax.

True. On the other hand, that article builds a single model, while the
articles I cited above are more ambitious and would give (among other
advantages) a large class of models, supposedly all the hypercomplete
infinity-toposes.

Moreove I still don't see any prospect of anyone writing non-trivial
formal ZFC code. The above articles use deductive systems (type
theories) which do lend themselves to formal coding and in which
formal coding is actually done in practice and not just hypothesized.
For instance the practical advantage of cubical sets over simplicial
sets is a practical insight gained by actually looking into the
formalization.

But of course if somebody comes up with a formalization in ZFC, I
won't complain. I might think that with the same effort much more
could have been accomplished in a more suitable environment. But
that's a matter of taste and need not further concern us here.