completed publication data for:

- Steve Awodey,
*Type theory and homotopy*, p. 183-201 in: Dybjer P., Lindström S., Palmgren E., Sundholm G. (eds.),*Epistemology versus Ontology*, Springer 2012 (arXiv:1010.1810, doi:10.1007/978-94-007-4435-6_9)

@Mike thanks!

]]>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.

]]>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.

]]>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.

]]>upon request, I added pointer to p. 9 of

- Chris Kapulkin, Peter Lumsdaine,
*The homotopy theory of type theories*, Advances in Mathematics Volume 337, 15 October 2018, Pages 1-38 (arXiv:1610.00037)

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

steveawodey

]]>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.

]]>And what was Steve’s comment?

]]>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.

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

]]>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?

]]>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.

]]>