Re: [HoTT] Geometry in Modal HoTT now on Youtube

[Egbert Rijke <e.m.rijke@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2558 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 3891 bytes --]