Post #1490089
2026-04-12 16:23 UTC
Is there a left adjoint to Nakano's later modality? It would be nice to handle it MTT style as a positive modality, rather than just have it as an applicative functor.
Perhaps it needs linearity in order to work though, because it's not a monad...
@danielgratzer @bentnib
Replies (3)
-
@pamorim@mathstodon.xyz 2026-04-12 16:30
@olynch @danielgratzer @bentnib https://arxiv.org/pdf/1208.3596 section 2.1
-
@jonmsterling@mathstodon.xyz 2026-04-12 16:43
@olynch @danielgratzer @bentnib There’s several papers doing this in MTT… I think the coolest one is here: https://www.danielgratzer.com/papers/a-modal-deconstruction-of-loeb-induction.pdf
-
@danielgratzer@mathstodon.xyz 2026-04-12 17:29
@olynch @bentnib Even more: there is an infinite chain of adjoints extending to the left from the later modality!