From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 3528 invoked from network); 27 Feb 2021 10:44:01 -0000 Received: from mail-yb1-xb3a.google.com (2607:f8b0:4864:20::b3a) by inbox.vuxu.org with ESMTPUTF8; 27 Feb 2021 10:44:01 -0000 Received: by mail-yb1-xb3a.google.com with SMTP id b127sf346570ybc.13 for ; Sat, 27 Feb 2021 02:44:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=CSyupyBQgpGPz49sepGr52X3Kv54S/FRO3Kfef2rjk4=; b=IVzAf3XeGCoKluLOy0GNajZ7kRXhzOe3G9XiaU/FuB0NYCt9UR5hz1MUsE6LwHKPcx roGEH77/jBdPHCZbZ53Pxx2fFFvWQZ9DGHDZ9RHboYZsRwG/wDKWZ9S6W9yhOQDquN5p WF5LAebp5TlY2B4HGQCRNrEWYqU3ymSS5ABH/y0vap0ag624HW0w6aPUxtSyZRS75ZNF m0h86w1E5LXGh/M/xcmnjKEZegxKH/ka6rJ8XZYU1cq/NzeZjAfSAFRrC6ki6Va+s1Qc UIRwLryHZTR73wEveMWGXfFk6bBg35LqI38Qp5L1ODiOdaoYK1POnkjcMQw4zRWz/qib fy9g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=CSyupyBQgpGPz49sepGr52X3Kv54S/FRO3Kfef2rjk4=; b=Car9QyQ9yJKqmctrJvZCfK+Adx7AeuvYVmBQCHoU1zha1T6cT2iicStn3uddaLcWaK ou5gLrTBg+skrhkQjXlBlio0RuLuvDYWUlKVdB8fcVqhI/jlO8Ym4kbZThqTpQ4uge1v /1o7pFeeabin44ON6BpqpZGwiUeSSSA5dzr7UovX+bplW3+0PVqlobIogAE/tM3gr3di ls2pulv7F5uJbCkTEY7tkCrchVK3fwSC0wfQpBIdnWcyhXMYq/m0meG0FqZjfbQ83uwE 8pQVqstef5UaJS/rbtwl0vvnpGMlTaCxxavNqoCRpT6shr4B5egUjopZZpOC+QxiyK6R Yj9g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=CSyupyBQgpGPz49sepGr52X3Kv54S/FRO3Kfef2rjk4=; b=mFdbXXQ0RKVScCDWAGLrFO50t3RgN0JtQ6UQk2NbLJjegme1dK19nZ/4vcO0a3IPYu GCmTPcpxtKKkDon8uB8wORpDcjCnV2A5cCqHFzGH91BS4TT0+MBKyzOpf11u7ejqyzVL xrQP3OfwqKb4WiXBpgZVj8WVZ41yONP+PXU459NbO5M9D2hE8TGcp6BGvgYOUKc2MH1E 2xIa4lsaG6xeqN7pXMkQWmdbrxqgP4Cjfce49Exhs87+8JuurlpWkljHRM3tZwR9FtJK D6tmkGLwkVHeU+GxrVOz7sNKlY/xvEgYunniiXpC2mAlGbXedG+aXy06Z5YibuFw+GZh 7g1A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532n71KuvMMc9JfAlO71HgpJJb3bKUwxl0k4RbCKB8uuebqbmf40 OkKWUj8rc4tsXncPtiWZwUs= X-Google-Smtp-Source: ABdhPJzRyL814ycC42YMKWyFy2Hj5m4lGbaGdp8ow2uxLb4jBUHf5N1kUB54TtKT8iglzCT0hTIIaQ== X-Received: by 2002:a25:1984:: with SMTP id 126mr9832611ybz.341.1614422636793; Sat, 27 Feb 2021 02:43:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:77c7:: with SMTP id s190ls3189415ybc.1.gmail; Sat, 27 Feb 2021 02:43:56 -0800 (PST) X-Received: by 2002:a25:16d4:: with SMTP id 203mr10464485ybw.80.1614422635991; Sat, 27 Feb 2021 02:43:55 -0800 (PST) Date: Sat, 27 Feb 2021 02:43:55 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: In-Reply-To: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> References: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> Subject: [HoTT] Re: Foundational question about a large set of small sets MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1596_560630603.1614422635318" X-Original-Sender: UlrikBuchholtz@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_1596_560630603.1614422635318 Content-Type: multipart/alternative; boundary="----=_Part_1597_849511262.1614422635318" ------=_Part_1597_849511262.1614422635318 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Mart=C3=ADn, As you indicate, it is necessary to truncate: There can be no (large) set S= =20 and function (1) f : (X : Set U) =E2=86=92 (g : X =E2=86=92 S) =C3=97 is-emb g . If there was, you could apply f to swap : Bool =3D Bool, to get an embeddin= g=20 g : Bool =E2=86=92 S satisfying g =3D g =E2=88=98 swap, which is absurd. So how about having a set S and a function (2) f : (X : Set U) =E2=86=92 =E2=80=96 (g : X =E2=86=92 S) =C3=97 is-emb = g =E2=80=96 ? This is equivalent to having a (large) set V covering the groupoid Set U.= =20 Indeed, if p : V =E2=86=92 Set U is a surjection from a set V, we can take = S :=3D (v=20 : V) =C3=97 p v. Then if X : Set U, there merely exists v : V with a biject= ion h=20 : X =E2=89=83 p v. Composing with the inclusion at v, we get the desired em= bedding=20 g. Conversely, if we have S and f as in (2), then we can take V :=3D (X : Set = U)=20 =C3=97 (g : X =E2=86=92 S) =C3=97 is-emb g, the set of U-small subsets of S= . Then the first=20 project, p, is surjective by (2). Unfortunately, I don't know of a model where there's no set cover of Set U.= =20 The counter-model at the nLab for the general statement that sets cover=20 groupoids (https://ncatlab.org/nlab/show/n-types+cover#InModels), using=20 presheaves on the category-join B=C2=B2=E2=84=A4 * 1, doesn't work for this= purpose,=20 AFAICT. (Using a general 2-group G and presheaves on BG * 1 won't help=20 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 =F0=9D=93=A4=E2=81=BA that embeds = all sets in > the universe =F0=9D=93=A4? > > 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 =F0=9D=93=A4 can be embedded into the type of all ordin= als. But > notice that this is a (necessarily) propositionally truncated > mathematical statement in HoTT/UF. > > Can you find a set in the successor universe =F0=9D=93=A4=E2=81=BA that e= mbeds all sets > in the universe =F0=9D=93=A4? (Say from the material available in the HoT= T book.) > > Martin > > --=20 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 e= mail 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= . ------=_Part_1597_849511262.1614422635318 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Mart=C3=ADn,

As you indicate, it is nece= ssary to truncate: There can be no (large) set S and function
(1)  f : (X : Set U) =E2=86=92 (g : X =E2=86=92 S) =C3=97 = is-emb g .

If there was, you could apply f to swap= : Bool =3D Bool, to get an embedding g : Bool =E2=86=92  S satisfying= g =3D g =E2=88=98 swap, which is absurd.

So how a= bout having a set S and a function

(2)  f : (= X : Set U) =E2=86=92 =E2=80=96 (g : X =E2=86=92 S) =C3=97 is-emb g =E2=80= =96 ?

This is equivalent to having a (large) s= et V covering the groupoid Set U. Indeed, if p : V =E2=86=92 Set U is a sur= jection from a set V, we can take S :=3D (v : V) =C3=97 p v. Then if X : Se= t U, there merely exists v : V with a bijection h : X =E2=89=83 p v. Compos= ing 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 := =3D (X : Set U) =C3=97 (g : X =E2=86=92 S) =C3=97 is-emb g, the set of U-sm= all subsets of S. Then the first project, p, is surjective by (2).

Unfortunately, I don't know of a model where there's no se= t cover of Set U. The counter-model at the nLab for the general statement t= hat sets cover groupoids (https://ncatlab.org/nlab/show/n-types+cover#InMod= els), using presheaves on the category-join B=C2=B2=E2=84=A4 * 1, doesn't w= ork 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 e= scardo...@gmail.com wrote:
Is there a set in a successor universe =F0=9D=93=A4=E2=81=BA = that embeds all sets in
the universe =F0=9D=93=A4?

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 =F0=9D=93=A4 can be embedded into the type of all ord= inals. But
notice that this is a (necessarily) propositionally truncated
mathematical statement in HoTT/UF.

Can you find a set in the successor universe =F0=9D=93=A4=E2=81=BA that= embeds all sets
in the universe =F0=9D=93=A4? (Say from the material available in the H= oTT book.)

Martin

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/c10d88b0-8856-4a35-b71d-c2f9d36b5f7an%40googl= egroups.com.
------=_Part_1597_849511262.1614422635318-- ------=_Part_1596_560630603.1614422635318--