[FOM] New Umbrella?

Urs Schreiber urs.schreiber at googlemail.com
Tue Oct 28 15:43:49 EDT 2014

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!


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:


More information about the FOM mailing list