Dear Martín,
As you indicate, it is necessary to truncate: There can be no (large) set S and function
(1) f : (X : Set U) → (g : X → S) × is-emb g .
If there was, you could apply f to swap : Bool = Bool, to get an embedding g : Bool → S satisfying g = g ∘ swap, which is absurd.
So how about having a set S and a function
(2) f : (X : Set U) → ‖ (g : X → S) × is-emb g ‖ ?
This is equivalent to having a (large) set V covering the groupoid Set U. Indeed, if p : V → Set U is a surjection from a set V, we can take S := (v : V) × p v. Then if X : Set U, there merely exists v : V with a bijection h : X ≃ p v. Composing with the inclusion at v, we get the desired embedding g.
Conversely, if we have S and f as in (2), then we can take V := (X : Set U) × (g : X → S) × is-emb g, the set of U-small subsets of S. Then the first project, p, is surjective by (2).
Unfortunately, I don't know of a model where there's no set cover of Set U. The counter-model at the nLab for the general statement that sets cover groupoids (https://ncatlab.org/nlab/show/n-types+cover#InModels), using presheaves on the category-join B²ℤ * 1, doesn't work for this purpose, AFAICT. (Using a general 2-group G and presheaves on BG * 1 won't help either, I think.)
Cheers,
Ulrik
On Friday, February 26, 2021 at 9:33:29 PM UTC+1 escardo...@gmail.com wrote:
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/c10d88b0-8856-4a35-b71d-c2f9d36b5f7an%40googlegroups.com.