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,EgbertOn 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?JonasOn 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 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,EgbertOn 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 workshopto 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,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.
--
--
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.
--
--