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.
What of the elementary/Grothendieck distinction? Who first articulated claims about what this distinction means for the internal logic?
And when do we get to see slides, or better a recording, Mike?
Here are the slides of Mike’s second talk. I don’t think there exists a better recording apart from the one Felix took.
So the strict univalent universes correspond to which type universes out of: Russell, Tarski, weak Tarski ? I guess not the last… Or is this an orthogonal notion? This should be made explicit in the page where Mike’s results are discussed.
And what was Steve’s comment?
Steve just highlighted that it’s a breakthrough (on the off-chance that anyone didn’t get it) and amplified that it finally goes to confirm his 10 year old conjecture.
upon request, I added pointer to p. 9 of
Re #4, I would say these universes correspond most directly to strictly Tarski ones, although the distinction between Russell and strict-Tarski universes is mostly lost when passing from syntax to categorical models (even strict ones such as CwFs). I think the usual way to interpret Russell universes is to first “desugar” them to Tarski universes and then interpret those.
I don’t have time to add it right now, but we should also be clear about the difference between the conjectures “type theory can be interpreted in all Grothendieck $(\infty,1)$-toposes” and “the homotopy theory of type theories is equivalent to the homotopy theory of elementary $(\infty,1)$-toposes”. The former is what I announced, but the latter is still quite open, although Kapulkin-Sumilo have proven the analogue for $(\infty,1)$-categories with finite limits, corresponding to type theories with $\Sigma$ and identity types only, no $\Pi$s or universes, and it seems likely that the tools I used in the Grothendieck case may be useful in proving versions of the stronger conjecture.
Also here are my slides from the Midwest HoTT last weekend, which have some more detail. I’m hoping to put up the preprint within a week or two.
@Mike thanks!
1 to 12 of 12