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

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2798 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 3560 bytes --]