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 6092 invoked from network); 28 Feb 2021 12:45:18 -0000 Received: from mail-yb1-xb3f.google.com (2607:f8b0:4864:20::b3f) by inbox.vuxu.org with ESMTPUTF8; 28 Feb 2021 12:45:18 -0000 Received: by mail-yb1-xb3f.google.com with SMTP id v6sf16029262ybk.9 for ; Sun, 28 Feb 2021 04:45:18 -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=pMO+ZjiEtppfx8jCnfemxoQR/vzkTgu6jCTwGEHY0xQ=; b=QBhNmXupLKzVl87vr4TuSy02LlUmiWJ6jI7JV+Qnd8pJcrBtI77q5HcsM7DcybLauO HZGhJCIj1oTNR9YeUMzpf/0sCP1+4O8t+p58VYGXLfMR7DGdk/2pqDFA4VrWpYfy+EwO lft9OK9nZ3aoAr8Tnl/CI9BFy8y5N/0JdJIwI/fESvqNYnKQzHhQrXjk1SpYyxEb67Jf 9fqZsqxLgO5wDkZnVNLpdMFUULoYwKNexDrQvX2sx2KO4nQ5bN5WO3RvtryAqErjbxpA zz/iWBiHbbkopAGedNyL/2f9eo9q8UC6yNDJc5HdC5t8rzOZUySo0FV4jJgLwW1pkQo8 OwTg== 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=pMO+ZjiEtppfx8jCnfemxoQR/vzkTgu6jCTwGEHY0xQ=; b=E4v7klsfyjXjqMXcmGDZrl3T7l71pn5DjcDiqNXv88ntjnt2mJ7xu4Wlo8X11Zi+uN j4hGhCy6QVLelDOcC8MA0b2CQgIdwXBPM6pqCTbjOdwNfq8TV+9gwTHbpcUlN82iDiZn dXLKo3WEbaPkOiTDezhXDy9HOuIGTj/iYl+1Z9VTZdBYMTm3ZxtCqrrIVJqJu3ozDbAl vZs9NK4aumGkLIkILPxPdFCMvolUuep0vj9V4QSSlQa8xB8mIo10zoZ7e98n4QoaszKu pAuNCTuMBK1TanYAVUvAU1ScFryLxjpXF6q9ZBYFfC2zpCTzUyUkCiZgpolrOmzcERdw fQ3A== 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=pMO+ZjiEtppfx8jCnfemxoQR/vzkTgu6jCTwGEHY0xQ=; b=dPOIGO86LjBGY3iejTindjQFnyJXNslkvsTPg4Bh5CK6vF6JpeiUlQ1iizvuoyM7wq zo3ASPFTlcr08WYX6x8Znx4H2nys/N3zzp+NhTPQF/kdr9WReWZdP8U7A5kjpKUlRueI IMOSRvak/8sFwMcrmYdUAyCOSv5+/RxuKjZja03EPV6uLGPTV/SJ5zKzprXGhlbz6+n2 ZeDsJcpVVDhGBuNfVhrH/35zzpanj9cUhsLvqrsO15/Ale2Y6tHwgWZogsdh2do5vNOc 9YoB9OpWNRljhXp1Pl1aC8LtFBXRk2k4aXycJl6HelBQ11vkOe7Uim9FA8MN043l9bp/ ksng== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531lizx2Wj8E0/EUsjn7mchBri30TJPkrif4B7Eqr+etjTKZM+UW Z42j0hO3KK8gCpn2Ucf54CI= X-Google-Smtp-Source: ABdhPJygAHt9LXunkvYwAligKoKlEKlXTNBamWtu7fOUwQnrunnz6Bs8WNV+ReJsD2HKMALGf6pYsg== X-Received: by 2002:a25:830e:: with SMTP id s14mr17495779ybk.42.1614516310986; Sun, 28 Feb 2021 04:45:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:7807:: with SMTP id t7ls6756021ybc.10.gmail; Sun, 28 Feb 2021 04:45:10 -0800 (PST) X-Received: by 2002:a25:4454:: with SMTP id r81mr15497617yba.189.1614516310158; Sun, 28 Feb 2021 04:45:10 -0800 (PST) Date: Sun, 28 Feb 2021 04:45:09 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: In-Reply-To: References: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> Subject: Re: [HoTT] Re: Foundational question about a large set of small sets MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_410_244573411.1614516309536" 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_410_244573411.1614516309536 Content-Type: multipart/alternative; boundary="----=_Part_411_1794262075.1614516309536" ------=_Part_411_1794262075.1614516309536 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=20 > Set" is presheaves on the 2-category X with two objects a and b,=20 > X(b,a)=3D0, X(a,a)=3D1, and X(b,b) =3D X(a,b) =3D B=E2=84=A4. Thanks for the hint! Let me see if I can work it out: =20 We let G =3D B=E2=84=A4, considered as a 2-group with delooping BG =3D B=C2= =B2=E2=84=A4. Write * for=20 the basepoint. Take =E2=88=82 : BG =E2=86=92 U, =E2=88=82 t =3D (* =3D t). We get the dire= ct category X by attaching=20 to the terminal category 1 a new level of objects BG along the boundary=20 operator =E2=88=82. (We could make another direct category using =E2=88=82 t =3D (t =3D t); thi= s also=20 works!) The object a is the unique object at level 0; write b(t), t : BG, for the= =20 objects at level 1. Contexts =CE=93 =E2=8A=A2 : =CE=93=E2=82=80 : U =CE=93=E2=82=81 : (t : BG) =E2=86=92 (=E2=88=82 t =E2=86=92 =CE=93=E2=82=80= ) =E2=86=92 U Representable contexts a and b(t), t : BG : a=E2=82=80 =3D 1 a=E2=82=80 t u =3D 0 b(t)=E2=82=80 =3D =E2=88=82 t =3D (* =3D t) b(t)=E2=82=81 t' u =3D (q : t' =3D t) =C3=97 (u =3D_q id) Evaluation of =CE=93 at a is =CE=93=E2=82=80, evaluation at b(t), t : BG, i= s =CE=93(t) =3D (u : =E2=88=82 t =E2=86=92 =CE=93=E2=82=80) =C3=97 =CE=93=E2= =82=81 t u (So =CE=93 evaluates to sets iff =CE=93=E2=82=80 and =CE=93=E2=82=81 are Se= t-valued) Substitutions =CF=83 : =CE=93 =E2=86=92 =CE=94 : =CF=83=E2=82=80 : =CE=93=E2=82=80 =E2=86=92 =CE=94=E2=82=80 =CF=83=E2=82=81 : (t : BG) =E2=86=92 (u : =E2=88=82 t =E2=86=92 =CE=93=E2= =82=80) =E2=86=92 =CE=93=E2=82=81 t u =E2=86=92 =CE=94=E2=82=81 t (=CF=83= =E2=82=80 =E2=88=98 u) Action of =CF=83 on values at b(t), t : BG : =CF=83(t) : =CE=93(t) =E2=86=92 =CE=94(t) =CF=83(t) (u , =CE=B3) =3D (=CF=83=E2=82=80 =E2=88=98 u , =CF=83=E2=82=81 t= u =CE=B3) Families =CE=93 =E2=8A=A2 A : A=E2=82=80 : =CE=93=E2=82=80 =E2=86=92 U A=E2=82=81 : (t : BG) =E2=86=92 (u : =E2=88=82 t =E2=86=92 =CE=93=E2=82=80)= =E2=86=92 =CE=93=E2=82=81 t u =E2=86=92 ((x : =E2=88=82 t) =E2=86=92 A=E2= =82=80 (u x)) =E2=86=92 U Universe of sets, Set =E2=8A=A2 : Set=E2=82=80 =3D Set Set=E2=82=81 t u =3D ((x : =E2=88=82 t) =E2=86=92 u x) =E2=86=92 Set hence value over b(t) is: Set(t) =3D (u : =E2=88=82 t =E2=86=92 Set) =C3=97 (((x : =E2=88=82 t) =E2= =86=92 u x) =E2=86=92 Set) (I think this is correct; I'm skipping the entire calculation of the=20 interpretation of (A : U) =C3=97 is-set A. We really only need the level ze= ro=20 component, and that's definitely Set.) Now assume there is a set context =CE=93 and a levelwise surjection =CF=83 = : =CE=93 =E2=86=92 Set : =CF=83=E2=82=80 : =CE=93=E2=82=80 =E2=86=92 Set (i.e., a cover of Set at t= he meta-level) =CF=83=E2=82=81 : (t : BG) =E2=86=92 (u : =E2=88=82 t =E2=86=92 =CE=93=E2= =82=80) =E2=86=92 =CE=93=E2=82=81 t u =E2=86=92 ((x : =E2=88=82 t) =E2=86= =92 =CF=83=E2=82=80 (u x)) =E2=86=92 Set so we assume that =CF=83(t) : =CE=93(t) =E2=86=92 (v : =E2=88=82 t =E2=86=92 Set) =C3=97 (((x= : =E2=88=82 t) =E2=86=92 v x) =E2=86=92 Set) =CF=83(t) (u , =CE=B3) =3D (=CF=83=E2=82=80 =E2=88=98 u , =CF=83=E2=82=81 t= u =CE=B3) is surjective for each t : BG. This is a proposition, so it holds iff it holds at the basepoint * : BG. We have =E2=88=82 * =3D (* =3D *) =3D G =3D B=E2=84=A4, so v : B=E2=84=A4 = =E2=86=92 Set amounts to a set with an=20 automorphism. However, any u : B=E2=84=A4 =E2=86=92 =CE=93=E2=82=80 is constant, since = =CE=93=E2=82=80 is a set, so a non-trivial v=20 cannot be written as =CF=83=E2=82=80 =E2=88=98 u for any such u. Nice! One can then get a=20 > counter-model to "there merely exists a set that covers Set" with=20 > presheaves on X * 1. This I didn't check. But couldn't we here instead appeal to homotopy=20 canonicity? Since Set is a closed type, if there is a proof of the mere=20 existence of a set cover of Set, we could extract a specific term for one,= =20 and then obtain a contradiction in the above model. Cheers, Ulrik --=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/b3e72012-1aa4-44f7-b2e6-ab83ebe7b9bfn%40googlegroups.com= . ------=_Part_411_1794262075.1614516309536 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sunday, February 28, 2021 at 12:00:29 AM UTC+1 Mike wrote:
I beli= eve 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)=3D0, X(a,a)=3D1, and X(b,b) =3D X(a,b) =3D B=E2=84=A4.

Thanks for the hint! Let me see if I can work it out= :
 
We let G =3D B=E2=84=A4, considered as a 2= -group with delooping BG =3D B=C2=B2=E2=84=A4. Write * for the basepoint.Take =E2=88=82 : BG =E2=86=92 U, =E2=88=82 t =3D (* =3D t). We get the di= rect category X by attaching to the terminal category 1 a new level of obje= cts BG along the boundary operator =E2=88=82.
(We could make another dir= ect category using =E2=88=82 t =3D (t =3D t); this also works!)
The obje= ct a is the unique object at level 0; write b(t), t : BG, for the objects a= t level 1.

Contexts =CE=93 =E2=8A=A2 :

=CE=93=E2=82=80 : U
=CE=93=E2=82=81 : (t : BG) =E2=86= =92 (=E2=88=82 t =E2=86=92 =CE=93=E2=82=80) =E2=86=92 U

Representabl= e contexts a and b(t), t : BG :

a=E2=82=80 =3D= 1
a=E2=82=80 t u =3D 0

b(t)=E2=82=80 =3D =E2=88=82 t =3D (* =3D = t)
b(t)=E2=82=81 t' u =3D (q : t' =3D t) =C3=97 (u =3D_q id)

Eval= uation of =CE=93 at a is =CE=93=E2=82=80, evaluation at b(t), t : BG, is

=CE=93(t) =3D (u : =E2=88=82 t =E2=86=92 =CE=93= =E2=82=80) =C3=97 =CE=93=E2=82=81 t u

(So =CE=93 evaluates to sets i= ff =CE=93=E2=82=80 and =CE=93=E2=82=81 are Set-valued)

Substitutions= =CF=83 : =CE=93 =E2=86=92 =CE=94 :

=CF=83=E2= =82=80 : =CE=93=E2=82=80 =E2=86=92 =CE=94=E2=82=80
=CF=83=E2=82=81 : (t = : BG) =E2=86=92 (u : =E2=88=82 t =E2=86=92 =CE=93=E2=82=80) =E2=86=92 =CE= =93=E2=82=81 t u =E2=86=92 =CE=94=E2=82=81 t (=CF=83=E2=82=80 =E2=88=98 u)<= br>
Action of =CF=83 on values at b(t), t : BG :

=CF=83(t) : =CE=93(t) =E2=86=92 =CE=94(t)
=CF=83(t) (u , =CE=B3) = =3D (=CF=83=E2=82=80 =E2=88=98 u , =CF=83=E2=82=81 t u =CE=B3)

Famil= ies =CE=93 =E2=8A=A2 A :

A=E2=82=80 : =CE=93= =E2=82=80 =E2=86=92 U
A=E2=82=81 : (t : BG) =E2=86=92 (u : =E2=88=82 t = =E2=86=92 =CE=93=E2=82=80) =E2=86=92 =CE=93=E2=82=81 t u =E2=86=92 ((x : = =E2=88=82 t) =E2=86=92 A=E2=82=80 (u x)) =E2=86=92 U

Universe of set= s, Set =E2=8A=A2 :

Set=E2=82=80 =3D Set
Set= =E2=82=81 t u =3D ((x : =E2=88=82 t) =E2=86=92 u x) =E2=86=92 Set
=

hence value over b(t) is:

= Set(t) =3D (u : =E2=88=82 t =E2=86=92 Set) =C3=97 (((x : =E2=88=82 t) =E2= =86=92 u x) =E2=86=92 Set)

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

Now assume there is a set context =CE=93= and a levelwise surjection =CF=83 : =CE=93 =E2=86=92 Set :
<= br>
=CF=83=E2=82=80 : =CE=93=E2=82=80 =E2=86=92 Set  (i.e., = a cover of Set at the meta-level)
=CF=83=E2=82=81 : (t : BG) =E2=86=92 (= u : =E2=88=82 t =E2=86=92 =CE=93=E2=82=80) =E2=86=92 =CE=93=E2=82=81 t u = =E2=86=92 ((x : =E2=88=82 t) =E2=86=92 =CF=83=E2=82=80 (u x)) =E2=86=92 Set=

so we assume that

=CF=83(t) : =CE=93(t) =E2=86=92 (v : =E2=88=82 t =E2=86=92 Set) =C3=97 ((= (x : =E2=88=82 t) =E2=86=92 v x) =E2=86=92 Set)
=CF=83(t) (u , =CE=B3) = =3D (=CF=83=E2=82=80 =E2=88=98 u , =CF=83=E2=82=81 t u =CE=B3)

is surjective for each t : BG.

This is a propositio= n, so it holds iff it holds at the basepoint * : BG.
We have =E2=88=82 *= =3D (* =3D *) =3D G =3D B=E2=84=A4, so v : B=E2=84=A4 =E2=86=92 Set amount= s to a set with an automorphism.
However, any u : B=E2=84=A4 =E2=86=92 = =CE=93=E2=82=80 is constant, since =CE=93=E2=82=80 is a set, so a non-trivi= al v cannot be written as =CF=83=E2=82=80 =E2=88=98 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 chec= k. 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 contradic= tion in the above model.

Cheers,
Ulr= ik

--
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/b3e72012-1aa4-44f7-b2e6-ab83ebe7b9bfn%40googl= egroups.com.
------=_Part_411_1794262075.1614516309536-- ------=_Part_410_244573411.1614516309536--