[FOM] New umbrella?

Urs Schreiber urs.schreiber at googlemail.com
Tue Nov 4 13:07:43 EST 2014

On 11/2/14, Paul Levy <P.B.Levy at cs.bham.ac.uk> wrote:

>  Surely one cannot embed ZFC + universes  into HoTT, because HoTT refutes choice over a universe.

No, classical set theory with choice may be embedded into HoTT. One
imposes the classical axioms just on the 0-types (the sets), not on
the other types.


A model that interprets the resulting theory is, once more, the model
in simplical sets inside ZFC+inaccessibles. Here the 0-types are the
ordinary ZFC sets.

More information about the FOM mailing list