[FOM] New umbrella?

[Urs Schreiber]

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.

http://ncatlab.org/nlab/show/homotopy+type+theory+FAQ#IsHoTTLimitedToConstructiveMathematics

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.