[HoTT] Foundational question about a large set of small sets

[Martin Escardo <escardo.martin@gmail.com>]

Is there a set in a successor universe 𝓤⁺ that embeds all sets in
the universe 𝓤?

We can consider this question in models or in the language(s) of
HoTT/UF.

We can also consider this question constructively and
non-constructively.

I am interested in constructive answers in the languages of
HoTT/UF. But of course answers in the models and non-constructive
answers can illuminate the question I have in mind and so are welcome.

In the presence of the axiom of choice, every set can be well-ordered,
as proved in the HoTT book, and hence a non-constructive answer is
yes: every set in 𝓤 can be embedded into the type of all ordinals. But
notice that this is a (necessarily) propositionally truncated
mathematical statement in HoTT/UF.

Can you find a set in the successor universe 𝓤⁺ that embeds all sets
in the universe 𝓤? (Say from the material available in the HoTT book.)

Martin

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/034025b4-005d-79d1-cab1-67470b3245bd%40googlemail.com.