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 13998 invoked from network); 28 Feb 2021 14:01:40 -0000 Received: from mail-yb1-xb3c.google.com (2607:f8b0:4864:20::b3c) by inbox.vuxu.org with ESMTPUTF8; 28 Feb 2021 14:01:40 -0000 Received: by mail-yb1-xb3c.google.com with SMTP id 6sf16272503ybq.7 for ; Sun, 28 Feb 2021 06:01:39 -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=AIGFcBtSr2ROaOZEiQKRMpdnQjtfFs06JLxWQwB+n0g=; b=GUuLhKnfcf35HT3/1GwxNAZQSs3QADAS8Y+qgKgw7qSm/V2bA0a4sw30AloZLUvVum bNbqhO0x4eDssEqClgGQK6SYR6qp2wYvtVCsKnEUk738C6BdEKiKaY3bilG+Ru2kzTU9 jYQ+nDscZ0Tm23e9ZM1NQS3gWrcG3hlq31cUvY9GhCEex/5w46uibjRI46qre+qJxq9K 7qut8w96LDwsDucubZL65HQcItRlwd3gVzcRZ2ze48Hvmc5ZQ4UeRkitLd+T9lM4y16y sD9UeR/5yxh+UDIJP8YwzElVeFad+z1YSR8a2G0bbfPFi4ack/OkQ4l9HVPQsNRHn/6U scwg== 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=AIGFcBtSr2ROaOZEiQKRMpdnQjtfFs06JLxWQwB+n0g=; b=tdNa/zvJAPA504l5OVbFPusXqVlNbXfrf/voDVFgaGD5t+9zE/A4fyzXGHUAyDV77s C4iAX6PKXeHbekWMO4x36Mzevm2ku7HgORvm2lhFf8EM+x6188kRBwP546QemS2HxtIV 9R5rGtidKwoA8odiSRA+86N2O25/Nwqf2Z/jbwDvgfOSoPiy8mGG28zVT/o7o3cGq3K9 JaRO8qEifQB9E1Y7bLbSLV8CyErqTZgHgJCu9hOOX8Hmj8cUXurBN7kJvUa1W2lMKfsR yF/jKBG+TEQuXM1uo0yCXKDPfYCTqfFzhOnilm28Gqeu2Rxzi7F2tehbAUQf1ocKlyDs k0dA== 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=AIGFcBtSr2ROaOZEiQKRMpdnQjtfFs06JLxWQwB+n0g=; b=oD1/BQqDZKFq5t/+UR49X0st7FgXs3KAvtSC/rEUF5wgOo5NTQKnE13iMZBFA+87Mk gHJKQ2U1+gBqb2DxunkIdd6q8SX2SlXj243Ue9/sv7yVSTPYYyeafaqPReT2vR+3e16v khrn10uqEKpPnc1DmwOe/kLSJUxsuvCPTaIcjvdhxp7DmxYnu4pMe1ZaXHUFwPtXdcWj thf8LwX4M2uiSETE9vrbF9nvnnUxCLEAnFyj/kxA1lC7bRht5KAi8b1eHIv8MkRMt44f MWzlBjiZNsw74zuzGygFLE1MgZHonAfK8w930Rp5O3FG0K1aDBDohYNMFO5tvYX5rwfO DsXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533K4BqZi+9yjcXZG4Dno0A1vABPPc/QCoKF5AQI7/E54abyMl+j fgDFOZN5cjUliCtiLyEQYz0= X-Google-Smtp-Source: ABdhPJyROS1HKoCmOkQs+YcpuUYzSMi8cE5Q0syC1W3blULUl+SV7X06pUsQcA8PMe9gcM+TD52hSw== X-Received: by 2002:a25:c105:: with SMTP id r5mr17100471ybf.413.1614520872849; Sun, 28 Feb 2021 06:01:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:5bc2:: with SMTP id p185ls6816941ybb.7.gmail; Sun, 28 Feb 2021 06:01:12 -0800 (PST) X-Received: by 2002:a25:ab32:: with SMTP id u47mr16842027ybi.46.1614520871946; Sun, 28 Feb 2021 06:01:11 -0800 (PST) Date: Sun, 28 Feb 2021 06:01:11 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <848b3f3b-045b-46e4-b661-f639abbafff7n@googlegroups.com> 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_1462_273962450.1614520871213" 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_1462_273962450.1614520871213 Content-Type: multipart/alternative; boundary="----=_Part_1463_1757813933.1614520871213" ------=_Part_1463_1757813933.1614520871213 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable PS. We don't actually need to endoequivalences at level 1. A simpler=20 counter-model is obtained via the 2-level direct category with two objects= =20 a,b, and Hom(a,b) =3D B=E2=84=A4. 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=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 *=20 > 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=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); t= his 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,= 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 iff =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) > > 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 = zero=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=20 > : > > =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 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=20 > v 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/848b3f3b-045b-46e4-b661-f639abbafff7n%40googlegroups.com= . ------=_Part_1463_1757813933.1614520871213 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
PS. We don't actually need to endoequivalences at level 1. A simpler c= ounter-model is obtained via the 2-level direct category with two objects a= ,b, and Hom(a,b) =3D B=E2=84=A4. 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 th= at 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:
=C2=A0
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 direct category X by attaching to the termi= nal category 1 a new level of objects BG along the boundary operator =E2=88= =82.
(We could make another direct category using =E2=88=82 t =3D (t =3D= t); this also works!)
The object a is the unique object at level 0; wri= te b(t), t : BG, for the objects at level 1.

Conte= xts =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 :
<= div>
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&#= 39; =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, 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 iff =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)

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 valu= e 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 en= tire calculation of the interpretation of (A : U) =C3=97 is-set A. We reall= y only need the level zero component, and that's definitely Set.)

Now assume there is a set context =CE=93 and a levelwise surje= ction =CF=83 : =CE=93 =E2=86=92 Set :

=CF=83= =E2=82=80 : =CE=93=E2=82=80 =E2=86=92 Set=C2=A0 (i.e., a cover of Set at th= e 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 if= f 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 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 cannot be w= ritten 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 check. But couldn't we here instead ap= peal to homotopy canonicity? Since Set is a closed type, if there is a proo= f 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 &= 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/848b3f3b-045b-46e4-b661-f639abbafff7n%40googl= egroups.com.
------=_Part_1463_1757813933.1614520871213-- ------=_Part_1462_273962450.1614520871213--