[FOM] New Umbrella?

[Urs Schreiber]

On 10/28/14, Monroe Eskew <meskew at math.uci.edu> wrote in small part:

> Just produce a formal proof that ZFC+inaccessibles (naturally)
> interprets HoTT, and then apply this result to any future deductions from
> HoTT.  Maybe this is actually worth doing!

Indeed!

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