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

[HoTT] 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

-- 
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.

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

[Ulrik Buchholtz]

[-- 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 --]

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

[Michael Shulman]

On Sat, Feb 27, 2021 at 2:43 AM Ulrik Buchholtz
<ulrikbuchholtz@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

-- 
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/CAOvivQzawyMqT4uZ7%2BKbB_PftqbMzB4V8HUvgpJPSoe32p62aw%40mail.gmail.com.

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

[Ulrik Buchholtz]

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

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

-- 
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/b3e72012-1aa4-44f7-b2e6-ab83ebe7b9bfn%40googlegroups.com.

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

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

[Ulrik Buchholtz]

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

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

On Sunday, February 28, 2021 at 1:45:09 PM UTC+1 Ulrik Buchholtz wrote:

> 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
>
>

-- 
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/848b3f3b-045b-46e4-b661-f639abbafff7n%40googlegroups.com.

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

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

[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
<ulrikbuchholtz@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.)

-- 
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/CAOvivQxadLL6w0FehP3owkF%3DHP5vr%3Da3tcqm3FA_hGbrcOZjqA%40mail.gmail.com.

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

[Martin Escardo]

Interesting, Ulrik and Mike. Thanks! Martin

On 28/02/2021 15:13, Michael Shulman wrote:
> 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
> <ulrikbuchholtz@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.)
> 

-- 
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/b21281e6-2de2-c126-f139-b7df3107078f%40gmail.com.