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, 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 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.