* Re: [HoTT] Geometry in Modal HoTT now on Youtube
[not found] ` <CAGqv1OA0FxK=sw7CTiyV=1aDn60OU3CpL4b7W3UBaOQcjd2VgA@mail.gmail.com>
@ 2019-03-19 4:42 ` Egbert Rijke
0 siblings, 0 replies; 3+ messages in thread
From: Egbert Rijke @ 2019-03-19 4:42 UTC (permalink / raw)
To: Jonas Frey, Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 6303 bytes --]
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 <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.rijke@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.com>
>> wrote:
>>
>>> Hi Jonas,
>>>
>>> The last question is easiest: I do everything internally, so maybe it is
>>> 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 terminal
>>> projection is in the right class. Then by factoring the terminal projection
>>> 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 proof 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 class is
>>> closed under composition, 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.
>>>
>>> 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 <jonas743@gmail.com> wrote:
>>>
>>>> Hi Egbert (answering privately),
>>>>
>>>> I think that's weird since at least in the 1-categorical setting, every
>>>> reflection on say a locally presentable category determines a reflective
>>>> 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 ∞-presentable categories so e.g. there's a
>>>> reflective facsys whose left class consists of those maps that are inverted
>>>> 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 <e.m.rijke@gmail.com> wrote:
>>>>
>>>>> Dear all,
>>>>>
>>>>> During my lecture on modal descent someone in the audience (my
>>>>> apologies, I forgot who it was) asked the question
>>>>> <https://www.youtube.com/watch?v=InaRkqKdyp4&t=900s> whether
>>>>> 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).
>>>>>
>>>>> During the lecture I didn't know the answer, but now I do: It is
>>>>> indeed the case that modalities are equivalently described as reflective
>>>>> factorization systems. I wanted to attach hand-written notes containing the
>>>>> proof, but the files are too large to be contained in a message to this
>>>>> 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 slightly).
>>>>>
>>>>> 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 <felix.wellen@gmail.com>
>>>>> wrote:
>>>>>
>>>>>> Dear all,
>>>>>>
>>>>>> I just finished uploading the recordings of last week's workshop
>>>>>>
>>>>>> Geometry in Modal HoTT
>>>>>> <http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html#schedule>
>>>>>>
>>>>>> to youtube <https://www.youtube.com/channel/UCfQdw845tAduRwW6FnWC9KQ>.
>>>>>> 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:
>>>>>>
>>>>>> 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, send
>>>>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>>>> For more options, visit https://groups.google.com/d/optout.
>>>>>
>>>>
>>>
>>>
>>
>> --
>> egbertrijke.com
>>
>
>
> --
> egbertrijke.com
>
--
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, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 10385 bytes --]
^ permalink raw reply [flat|nested] 3+ messages in thread