[FOM] New Umbrella?

[Monroe Eskew]

> 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#BezemCoquandHuber13>
> http://ncatlab.org/nlab/show/cubical+set#KaposiAltenkirch14 <http://ncatlab.org/nlab/show/cubical+set#KaposiAltenkirch14>
This paper seems more like what I had in mind:

http://arxiv.org/abs/1211.2851 <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.  Then create a program that will compile any formal HoTT proof into a Gödel code which can be input directly into the ZFC+2I machine so that for any formal HoTT proof p with code c, we get a formal proof in ZFC-infinity that c is a formal HoTT proof.  Once this is complete, we will have made formalizing HoTT theorems in ZFC+2 inaccessibles just as practical as formalizing them in formal HoTT / Coq.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141029/dff13df5/attachment-0001.html>