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