Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Eric’s CNRS Research Proposal is an interesting read. A couple of items I’d like to hear more about:
the terminal example of a polynomial monad turns out to be quite interesting: it is the universe Type of type theory itself, equipped with the operation of dependent sum $\Sigma$. (p. 8)
any dependent family $P:X \to Type$ can be used to generate a left exact modality in type theory. (p. 13)
It seems that first point is along the lines of the section polynomial monad: Relation to object classifiers.
@David the second point is Theorem 3.10 in arXiv:1706.07526.
Edit: No its not.
Ah OK, thanks.
No it’s not! It’s http://mathieu.anel.free.fr/mat/doc/Anel-LexLocalizations.pdf.
I see. So it’s about describing $(\infty, 1)$-toposes via presentations rather than sites (slide 69).
PSp [parameterized spectra] is arguably the main protagonist of ∞-topos theory (slide 20)
is a bold claim.
I see Mathieu in now based in Philosophy at CMU, and has some interesting reflections at his site.
has some interesting reflections at his site
I don’t think I’ve seen the following before!
Verdier duality, which is measure theory on topoi.
it’s about describing $(\infty, 1)$-toposes via presentations rather than sites
That’s one way of saying it. Another way to say it is that they’ve finally found the correct $\infty$-categorical notion of “site”.
Added
1 to 9 of 9