Foundational question about a large set of small sets

[Martin Escardo]

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

[Ulrik Buchholtz]

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

[Michael Shulman]

On Sat, Feb 27, 2021 at 2:43 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> 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.)

I believe a counter-model to "there is a specified set that covers
Set" is presheaves on the 2-category X with two objects a and b,
X(b,a)=0, X(a,a)=1, and X(b,b) = X(a,b) = Bℤ. One can then get a
counter-model to "there merely exists a set that covers Set" with
presheaves on X * 1. I worked this out a while ago but never got
around to writing it up; it uses the fact that since these are
"inverse EI categories", there is an explicit description of the
universe (http://arxiv.org/abs/1508.02410).

Mike

[Ulrik Buchholtz]

On Sunday, February 28, 2021 at 12:00:29 AM UTC+1 Mike wrote:

I believe a counter-model to "there is a specified set that covers
Set" is presheaves on the 2-category X with two objects a and b,
X(b,a)=0, X(a,a)=1, and X(b,b) = X(a,b) = Bℤ.

Thanks for the hint! Let me see if I can work it out:

 

We let G = Bℤ, considered as a 2-group with delooping BG = B²ℤ. Write * for the basepoint.
Take ∂ : BG → U, ∂ t = (* = t). We get the direct category X by attaching to the terminal category 1 a new level of objects BG along the boundary operator ∂.
(We could make another direct category using ∂ t = (t = t); this also works!)
The object a is the unique object at level 0; write b(t), t : BG, for the objects at level 1.

Contexts Γ ⊢ :

Γ₀ : U
Γ₁ : (t : BG) → (∂ t → Γ₀) → U

Representable contexts a and b(t), t : BG :

a₀ = 1
a₀ t u = 0

b(t)₀ = ∂ t = (* = t)
b(t)₁ t' u = (q : t' = t) × (u =_q id)

Evaluation of Γ at a is Γ₀, evaluation at b(t), t : BG, is

Γ(t) = (u : ∂ t → Γ₀) × Γ₁ t u

(So Γ evaluates to sets iff Γ₀ and Γ₁ are Set-valued)

Substitutions σ : Γ → Δ :

σ₀ : Γ₀ → Δ₀
σ₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → Δ₁ t (σ₀ ∘ u)

Action of σ on values at b(t), t : BG :

σ(t) : Γ(t) → Δ(t)
σ(t) (u , γ) = (σ₀ ∘ u , σ₁ t u γ)

Families Γ ⊢ A :

A₀ : Γ₀ → U
A₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → ((x : ∂ t) → A₀ (u x)) → U

Universe of sets, Set ⊢ :

Set₀ = Set
Set₁ t u = ((x : ∂ t) → u x) → Set

hence value over b(t) is:

Set(t) = (u : ∂ t → Set) × (((x : ∂ t) → u x) → Set)

(I think this is correct; I'm skipping the entire calculation of the interpretation of (A : U) × is-set A. We really only need the level zero component, and that's definitely Set.)

Now assume there is a set context Γ and a levelwise surjection σ : Γ → Set :

σ₀ : Γ₀ → Set  (i.e., a cover of Set at the meta-level)
σ₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → ((x : ∂ t) → σ₀ (u x)) → Set

so we assume that

σ(t) : Γ(t) → (v : ∂ t → Set) × (((x : ∂ t) → v x) → Set)
σ(t) (u , γ) = (σ₀ ∘ u , σ₁ t u γ)

is surjective for each t : BG.

This is a proposition, so it holds iff it holds at the basepoint * : BG.
We have ∂ * = (* = *) = G = Bℤ, so v : Bℤ → Set amounts to a set with an automorphism.
However, any u : Bℤ → Γ₀ is constant, since Γ₀ is a set, so a non-trivial v cannot be written as σ₀ ∘ u for any such u. Nice!

One can then get a
counter-model to "there merely exists a set that covers Set" with
presheaves on X * 1.

This I didn't check. But couldn't we here instead appeal to homotopy canonicity? Since Set is a closed type, if there is a proof of the mere existence of a set cover of Set, we could extract a specific term for one, and then obtain a contradiction in the above model.

Cheers,

Ulrik

[Ulrik Buchholtz]

PS. We don't actually need to endoequivalences at level 1. A simpler counter-model is obtained via the 2-level direct category with two objects a,b, and Hom(a,b) = Bℤ. Ulrik

[Michael Shulman]

Yes, that's it. And I guess you are right about leaving out the
endoequivalences at level 1.

On Sun, Feb 28, 2021 at 4:45 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
>> One can then get a
>> counter-model to "there merely exists a set that covers Set" with
>> presheaves on X * 1.
>
>
> This I didn't check. But couldn't we here instead appeal to homotopy canonicity? Since Set is a closed type, if there is a proof of the mere existence of a set cover of Set, we could extract a specific term for one, and then obtain a contradiction in the above model.

Sure, but it seems a bit overkill to appeal to a hammer like homotopy
canonicity when a simple presheaf countermodel would suffice.
(Although I suppose there may be people on this list to whom the
opposite would seem true....) The semantic argument is that in
presheaves on any category with a terminal object, the terminal object
is projective, and thus the "existence principle" holds: any closed
type whose propositional truncation is true is already globally
inhabited. (Of course, the semantic proof of canonicity is similar,
using projectivity of 1 in a gluing category.)

[Martin Escardo]

Interesting, Ulrik and Mike. Thanks! Martin