# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMar 13th 2019

now that Mike announced a proof, and hearing Steve’s comment, I felt it would be nice to have a name for conjecture (partially) proven thereby, for ease of communiucating it to the rest of the world. Just a start, please edit the entry as need be.

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeMar 13th 2019

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?

• CommentRowNumber3.
• CommentAuthorAli Caglayan
• CommentTimeMar 13th 2019

Here are the slides of Mike’s second talk. I don’t think there exists a better recording apart from the one Felix took.

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeMar 13th 2019

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.

• CommentRowNumber5.
• CommentAuthorDavidRoberts
• CommentTimeMar 13th 2019

And what was Steve’s comment?

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeMar 13th 2019

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.

1. this was not a precise conjecture, but more of a research proposal.

steveawodey

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeMar 14th 2019

upon request, I added pointer to p. 9 of

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeMar 14th 2019

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.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeMar 14th 2019

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.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeMar 14th 2019

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.

• CommentRowNumber12.
• CommentAuthorDavidRoberts
• CommentTimeMar 14th 2019

@Mike thanks!

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeOct 31st 2020
• (edited Oct 31st 2020)

completed publication data for: