[FOM] New umbrella?
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