From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53c.google.com (mail-ed1-x53c.google.com [IPv6:2a00:1450:4864:20::53c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2224f9f5 for ; Tue, 19 Mar 2019 04:43:08 +0000 (UTC) Received: by mail-ed1-x53c.google.com with SMTP id x29sf21070edb.17 for ; Mon, 18 Mar 2019 21:43:08 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1552970588; cv=pass; d=google.com; s=arc-20160816; b=zsOlfSEvn9M5p24WmnNnTMhoLZgTOOPOxwCg2L5QHPKzxe2kSUva9oziKWLjmM0Mi+ cvWzTFj+k+jcZjhRPoFADoKtMiIv48fXLQQKKeaOpCBCu9tbY1IJo6wsS1PSETMUWAMN PACimMBgMysWaMuMofoEouR5CbPyjE3i2UPc+LYOrnSdOwKA8jDSWp+WOh+fD8ZmyNBT b1eN6iWvrXUoRDv5/kEJJ8+mDIoIl95dvaKrpM9w8Kig4Oswp3elXeINOfWan0LC6D+s gLyMh/KasPywrYvcKOGzkQ8PCHgZHvH8FOZV0j2pq1f+Ym4rASiKQbRlXh/sIQYLInzl aqhQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=b95F2u4+ivb/lcApjpajA4D1BxrM/YaVv9mkOsr7Zfw=; b=I/C3G2FV4P4tUfzI/bExQyX6s3HLI3hfXwYqcMZQjI3sZpJIrio+qwsQbTkadsgJ+X 62uKcdgZ7OtAxW1NhYP2RtNBUwCdbT4ONzdeeTdEg3yS7Wj2wa9FiYo8zh2zWiQ/hKxc vvH6Gumh8sfull+Z2zzhemZhMtGcgOheGGhKiEnxW8QVzvcZJS9LClTDXozT663K1E6P c490Zm6Fq3x/wtrPVFEUIf90k/zu/HzMq0M1Ea9C/xAI4dTvlxG/vxZRVDJMyxX7FHzo a+UKG5J+zOHgH3SZSsXJs8ubrQObCho51Yf1/ukyi+kzjT2sMQNdIbciB+HMOks0WAnW jWAA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k9bMwhb2; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=b95F2u4+ivb/lcApjpajA4D1BxrM/YaVv9mkOsr7Zfw=; b=jIgMSEFZCwtFelztZ2ArE0TcvTz4KMzK1BXuzqHkv+0MRdrKrstInf1ItVijQkQzbF ZLznh0VtOSy+qKYWVavXb2UZJi6rFsDv9vxyWTRlZjAK+tCX02weH+dxAdz21GdLt/R/ 6/a8ZPVPwiHKpipBokrDoiHqrDrichLLPUdkttt1xbDT+jJKYvb28c4rWrwDr+yFNNxu kYhz0a44eFefftyKgLNvNHKo7K19XmuBB1CiPlfyOPESI4kv3ohZv7dttgJhoNk3xwR0 I3wG0dyOSiJ/xp9tEqhnOoYEBjFzVu2OIweWgUkmV9HgjgZfxws1QfyRuhLmjMrKKkMG QDBw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=b95F2u4+ivb/lcApjpajA4D1BxrM/YaVv9mkOsr7Zfw=; b=bV7HPED+4/p3kIQC3YYbJAWmIJumzNn992VCz1baKiNC82z8cA6NRmzvEIY5vLG8Kx wQ9fxfZCrOWhW9eiGJxjoxqrg/ie52pK1R6zpPYvWrlXGqTxgJSei1o+OwbOLcwqJoot t/R/pgzvQun6lZfqe7nq2YK0inCwNy2GdiGia0r8W/spknSOBDzBtdQKGv7GqQBTy0ol dBW9N0tlUKmP8DFM0kEfPHE2xY49RjPGUPjZN9lbl788O2vNjkX1Ua/OmXV8kiLCLQ9R h2PLheR6LQvQcJ2i3clhdKpnTSFtuaEE94EU3Nt4dhYLrsDRnPo3+/XD1UH1jxv/vPsR MNNA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=b95F2u4+ivb/lcApjpajA4D1BxrM/YaVv9mkOsr7Zfw=; b=OcV7eAbHzqeviGaYdnF8gnG8yWeCjkklHyR8wQ7+Fi6jjRbWqt0ywyYn1WJm/OVAzX QpQZtcgncCal6gFuXqToicYRPsHDxiowx3Zu0cYs2l+hnJTk8a6d4ALJmNM/zGKxrlan OfOnptmmuaBqXBQiRJfu9HCryi6RPByKZm2Q68NLsj5aX3M/G9x9f86fr3Vv4phn/evL H45Vg0GDA+U7Wgf61nSrCGB3MWUZOOPSXzt2aN0z816N9WVvOHzCfG2nCBHI2+2++CwR 5MgVAezZY5OR15zGJ5Cfv+ik50VtB1dy/kiHmerPAmyyUuLRlRp45G5IBK82yXOPhLR/ GrgQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUil1tSFKuQ0hqzJigA20ZJGnkplU1TEpu7xpw+uFBBGh16uRaR hPV4l8zZQ5dfyg7XrKlWXC4= X-Google-Smtp-Source: APXvYqw8B830lC5KVoNOhRIr0l6zfFL7pFOpx1Ps9vDZsHnwIfOEmA7aUc835q3b4WWg+YmRmLhT6A== X-Received: by 2002:a17:906:6314:: with SMTP id p20mr1339913ejk.2.1552970587858; Mon, 18 Mar 2019 21:43:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:18b2:: with SMTP id c18ls3643267ejf.1.gmail; Mon, 18 Mar 2019 21:43:07 -0700 (PDT) X-Received: by 2002:a17:906:4312:: with SMTP id j18mr2191617ejm.12.1552970587199; Mon, 18 Mar 2019 21:43:07 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1552970587; cv=none; d=google.com; s=arc-20160816; b=gs+vMk+f6Yz///+wUAvT+J6qGmo/G1U2Z8cpMbDfIPIOVgaAcskm5UYq+N/aSFJPgB wWukVxDWaH83OatouB8uG38+C6hNrb8ZS3ZMhBvrv5M3FuiavQlTVfn6HcYwvXjXk1/O v2pZSqawfT2lnPHAFXlMB6RTCTRSmGYRftMY2WIOuedeVSsxOIMVGijJFGXDU20hUnof dR+AXnl/+NzdTmaIldx3zRRSP4Z5u/jyc6xechQQnxQtVra8BGQik/xZmY83SiR2L8IK a/e0Etd7JJC8/0FZG55cTvc/Q06hxQf8XaICdy3nOu9AhmWDw5zNlill5WGkSrYu0d8P 2bkw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=gj1MGAkR+meTagEcqvcND/wpMcBm9xLSIS9s43PTPts=; b=tAF/Sc2saI254eRl/YzqdF2RFiJlFbTie7RmFeEE04CyRH4OglmwUjxSuNyTWcIAf9 5wn7E/9DZYLVjbGHTu7BtPyElvhu6hh4ZQ6ztKl7p0MJcc7SVhDTEkfflRWYw67lsXZ9 iileRbggOxNFsVmeFNZqo3a7NLC1iL60/A3dArLO3mzK3QtuxMksVsRWEyuwXvylbpua NoaB8LSs6W/T6E2dBfqySFUNxLQM6UJdDR+/CSLLS2ak4sRv5Albqe8yzZqc8/iAozTr QztfTXoXy98L0RaDxkiJYpHB1efvcCMOU2GvDygzzNzV7dQic3dhsE0puZdq13heN9Ur Lg4A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k9bMwhb2; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com. [2a00:1450:4864:20::32a]) by gmr-mx.google.com with ESMTPS id r37si454680edd.2.2019.03.18.21.43.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Mar 2019 21:43:07 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) client-ip=2a00:1450:4864:20::32a; Received: by mail-wm1-x32a.google.com with SMTP id z11so6670790wmi.0 for ; Mon, 18 Mar 2019 21:43:07 -0700 (PDT) X-Received: by 2002:a1c:c647:: with SMTP id w68mr1780994wmf.8.1552970586833; Mon, 18 Mar 2019 21:43:06 -0700 (PDT) MIME-Version: 1.0 References: <76b61890-3a9d-46c0-948b-454c2a7040dd@googlegroups.com> In-Reply-To: From: Egbert Rijke Date: Mon, 18 Mar 2019 23:42:55 -0500 Message-ID: Subject: Re: [HoTT] Geometry in Modal HoTT now on Youtube To: Jonas Frey , Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000002cc72e05846b24e8" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=k9bMwhb2; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --0000000000002cc72e05846b24e8 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Jonas found a flaw... Thanks Jonas! (and forget what I said above) With kind regards, Egbert On Mon, Mar 18, 2019 at 11:40 PM Egbert Rijke wrote: > So I guess you're right then... and I made a mistake. Thanks so much for > pointing it out! > > On Mon, Mar 18, 2019 at 11:33 PM Egbert Rijke wrote= : > >> Wait a minute... in the proof that it is Sigma-closed I do have the >> diagrams the wrong way around. Yikes! >> >> On Mon, Mar 18, 2019 at 11:27 PM Egbert Rijke >> wrote: >> >>> Hi Jonas, >>> >>> The last question is easiest: I do everything internally, so maybe it i= s >>> different for external factorization systems. That I don't know. >>> >>> The first thing to show is that from a reflective factorization system >>> you get a modality. The modal types are the types for which the termina= l >>> projection is in the right class. Then by factoring the terminal projec= tion >>> you get the modal operator. Let's call it L. This gives a reflective >>> subuniverse (I believe you have no problem with this fact, but the proo= f is >>> easy, by orthogonality). Then you need to show that this reflective >>> subuniverse is closed under Sigma. If you have a family of modal types = over >>> a modal type, then the Sigma should also be modal. Since the right clas= s is >>> closed under composition, it suffices to show that the projection map i= s a >>> right map. This can be done by showing that it is right orthogonal to a= ny >>> map in the left class. So indeed I claim that any reflective factorizat= ion >>> system gives rise to a modality in this way. >>> >>> Ah, and since this is now a private message I can attach the proof. >>> Hopefully it is not false... >>> >>> Best, >>> Egbert >>> >>> >>> >>> On Mon, Mar 18, 2019 at 11:15 PM Jonas Frey wrote: >>> >>>> Hi Egbert (answering privately), >>>> >>>> I think that's weird since at least in the 1-categorical setting, ever= y >>>> reflection on say a locally presentable category determines a reflecti= ve >>>> factorization system whose left class consists of those maps that are >>>> inverted by the reflection (that's in the cassidy-hebert-kelly paper).= I >>>> suppose that's also true for =E2=88=9E-presentable categories so e.g. = there's a >>>> reflective facsys whose left class consists of those maps that are inv= erted >>>> by localization at the degree two map of the circle. >>>> >>>> Are you saying that this rfsys is also the "formally etale facsys" of >>>> some modality? >>>> >>>> More generally, are you saying your claim also holds up for other >>>> infty-toposes than spaces? In this case, do you want the notion of >>>> factorization system to be understood internally? >>>> >>>> Jonas >>>> >>>> >>>> On Tue, 19 Mar 2019 at 00:01, Egbert Rijke wrote= : >>>> >>>>> Dear all, >>>>> >>>>> During my lecture on modal descent someone in the audience (my >>>>> apologies, I forgot who it was) asked the question >>>>> whether >>>>> reflective factorization systems (i.e. orthogonal factorization syste= ms for >>>>> which the left class satisfies the 3-for-2 property) also characteriz= e >>>>> modalities. I thought this was a very nice question, because we have = a >>>>> theorem like that for stable factorization systems (i.e. orthogonal >>>>> factorization systems for which the left class is stable under pullba= ck). >>>>> >>>>> During the lecture I didn't know the answer, but now I do: It is >>>>> indeed the case that modalities are equivalently described as reflect= ive >>>>> factorization systems. I wanted to attach hand-written notes containi= ng the >>>>> proof, but the files are too large to be contained in a message to th= is >>>>> google group. I'll write it up properly soon. >>>>> >>>>> In particular it follows that the poset of stable factorization >>>>> systems is the same as the poset of reflective factorization systems,= even >>>>> though there are subtle differences between the stable factorization = system >>>>> of a modality, and the reflective factorization system of a modality = (i.e. >>>>> under this equivalence the left and right classes have to change slig= htly). >>>>> >>>>> My lecture is available via the link Felix just shared. >>>>> >>>>> With kind regards, >>>>> Egbert >>>>> >>>>> On Mon, Mar 18, 2019 at 11:53 AM Felix Wellen >>>>> wrote: >>>>> >>>>>> Dear all, >>>>>> >>>>>> I just finished uploading the recordings of last week's workshop >>>>>> >>>>>> Geometry in Modal HoTT >>>>>> >>>>>> >>>>>> to youtube . >>>>>> I'm afraid the audio is not good, but with enough volume it should b= e >>>>>> possible to understand everything. >>>>>> You can get an overview of the talks on the abstracts-page: >>>>>> >>>>>> http://www.andrew.cmu.edu/user/fwellen/abstracts.html >>>>>> >>>>>> All the best, >>>>>> Felix >>>>>> >>>>>> -- >>>>>> 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. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>> >>>>> >>>>> >>>>> -- >>>>> egbertrijke.com >>>>> >>>>> -- >>>>> 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, sen= d >>>>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>> >>> >>> >> >> -- >> egbertrijke.com >> > > > -- > egbertrijke.com > --=20 egbertrijke.com --=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. For more options, visit https://groups.google.com/d/optout. --0000000000002cc72e05846b24e8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Jonas found a flaw...=C2=A0

Thanks Jonas!=C2=A0

(and forget what I said = above)

With kind regards,
Egbert

On= Mon, Mar 18, 2019 at 11:40 PM Egbert Rijke <e.m.rijke@gmail.com> wrote:
=
So I guess you're right then... and I made a mistake. = Thanks so much for pointing it out!

On Mon, Mar 18, 2019 at 11:33 PM Egbert = Rijke <e.m.rijk= e@gmail.com> wrote:
Wait = a minute... in the proof that it is Sigma-closed I do have the diagrams the= wrong way around. Yikes!

On Mon, Mar 18, 2019 at 11:27 PM Egbert Rijke <= e.m.rijke@gmail.co= m> wrote:
Hi Jonas,

The last question is easie= st: I do everything internally, so maybe it is different for external facto= rization systems. That I don't know.

The first= thing to show is that from a reflective factorization system you get a mod= ality. The modal types are the types for which the terminal projection is i= n the right class. Then by factoring the terminal projection you get the mo= dal operator. Let's call it L. This gives a reflective subuniverse (I b= elieve you have no problem with this fact, but the proof is easy, by orthog= onality). Then you need to show that this reflective subuniverse is closed = under Sigma. If you have a family of modal types over a modal type, then th= e Sigma should also be modal. Since the right class is closed under composi= tion, it suffices to show that the projection map is a right map. This can = be done by showing that it is right orthogonal to any map in the left class= . So indeed I claim that any reflective factorization system gives rise to = a modality in this way.=C2=A0

Ah, and since this i= s now a private message I can attach the proof. Hopefully it is not false..= .

Best,
Egbert

=

On Mon, Mar 18, 2019 at 11:15 PM Jonas Frey <jonas= 743@gmail.com> wrote:
Hi=C2=A0Egbert (answering privately),

I think= that's weird since at least in the 1-categorical setting, every reflec= tion on say a locally presentable category determines a reflective factoriz= ation system whose left class consists of those maps that are inverted by t= he reflection (that's in the cassidy-hebert-kelly paper). I suppose tha= t's also true for =E2=88=9E-presentable categories so e.g. there's = a reflective facsys whose left class consists of those maps that are invert= ed by localization at the degree two map of the circle.=C2=A0

Are you say= ing that this rfsys is also the "formally etale facsys" of some m= odality?

More generally, are you saying your claim also holds up for othe= r infty-toposes than spaces? In this case, do you want the notion of factor= ization system to be understood internally?

Jonas


On Tue, 19 Mar 2019 at 00:01, Egbert Rijke <e.m.= rijke@gmail.com> wrote:
<= div dir=3D"ltr">Dear all,

During my lecture on modal des= cent someone in the audience (my apologies, I forgot who it was)=C2=A0asked the question=C2=A0whether reflective = factorization systems (i.e. orthogonal factorization systems for which the = left class satisfies the 3-for-2 property) also characterize modalities. I = thought this was a very nice question, because we have a theorem like that = for stable factorization systems (i.e. orthogonal factorization systems for= which the left class is stable under pullback).

D= uring the lecture I didn't know the answer, but now I do: It is indeed = the case that modalities are equivalently described as reflective factoriza= tion systems. I wanted to attach hand-written notes containing the proof, b= ut the files are too large to be contained in a message to this google grou= p. I'll write it up properly soon.

In particul= ar it follows that the poset of stable factorization systems is the same as= the poset of reflective factorization systems, even though there are subtl= e differences between the stable factorization system of a modality, and th= e reflective factorization system of a modality (i.e. under this equivalenc= e the left and right classes have to change slightly).

=
My lecture is available via the link Felix just shared.

=
With kind regards,
Egbert

On Mon, Mar 18, 2= 019 at 11:53 AM Felix Wellen <felix.wellen@gmail.com> wrote:<= br>
Dear all,

I just finished uploading the recordings of last week's worksho= p


to youtube. I'm afraid the audio is not good, but with= enough volume it should be possible to understand everything.
You can get an overview of the talks on the abstracts-page:

All the best,
Fe= lix

--
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@googleg= roups.com.
For more options, visit https://groups.google.com/d/optout.


--

--
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@googleg= roups.com.
For more options, visit https://groups.google.com/d/optout.




--


--


--

--
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.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000002cc72e05846b24e8--