[-- Attachment #1.1: Type: text/plain, Size: 648 bytes --] Mike has released this new preprint on the arXiv: All (∞,1)-toposes have strict univalent universes <https://arxiv.org/abs/1904.07004> Quoting the abstract: Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞, 1)-toposes, just as higher-order logic is used for 1-toposes. :)) -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 935 bytes --]

On 16/04/2019 13:06, Ali Caglayan wrote: > Mike has released this new preprint on the arXiv: > > All (∞,1)-toposes have strict univalent universes > <https://arxiv.org/abs/1904.07004> > > Quoting the abstract: > > Thus, homotopy type theory can be used as a formal language for > reasoning internally to (∞, 1)-toposes, just as higher-order logic is > used for 1-toposes. This is awesome. Perhaps it deserves a short explanation (or at least listing) of the crucial steps gere in this list. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Here's a brief summary of the steps: 1. Every Grothendieck (∞, 1)-topos can be presented by an accessible left exact left Bousfield localization of an injective model structure on a category of enriched simplicial presheaves. 2. Such presentations are right proper Cisinski model categories, hence (as we already knew) model MLTT, even with many HITs, but not previously known to model universes. 3. The fibrations in an injective model structure have no explicit "cofibrantly generated" description in terms of a lifting property, but it turns out they do have a fairly explicit "algebraic" description in terms of the rectifiability of homotopy coherent natural transformations (a homotopical version of "coflexible algebras"). 4. Now define a presheaf U by U(x) = the set of injective fibrations over the representable C(-,x) *equipped with* such fibrancy structure (suitably rectified to become a strict presheaf), and we get a fibrant and univalent universe. 5. Finally, any accessible left exact localization can be presented internally by a lex modality (using the recent characterization thereof by Anel-Biedermann-Finster-Joyal), and the universe of modal types for a lex modality is modal, giving a universe for the localized model structure. For more detail, you can read the introduction to the paper (or the whole thing, of course), or look at these slides from last month's Midwest HoTT seminar: http://home.sandiego.edu/~shulman/papers/injmodel-talk.pdf On Wed, Apr 17, 2019 at 3:59 PM 'Martin Escardo' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: > > On 16/04/2019 13:06, Ali Caglayan wrote: > > Mike has released this new preprint on the arXiv: > > > > All (∞,1)-toposes have strict univalent universes > > <https://arxiv.org/abs/1904.07004> > > > > Quoting the abstract: > > > > Thus, homotopy type theory can be used as a formal language for > > reasoning internally to (∞, 1)-toposes, just as higher-order logic is > > used for 1-toposes. > > This is awesome. > > Perhaps it deserves a short explanation (or at least listing) of the > crucial steps gere in this list. > > Best, > Martin > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

I only had a rough glance at your paper. But as it seems you don't interpret directly in the infty toposes but rather in some representing model structure. No complaint because I don't expect otherwise. In any case it is quite an achievement to get universes "strongly `a la Tarski". Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Right, I would say that interpreting in a representing model structure is the limit of current technology. Maybe one day we'll be able to interpret directly in an infinity-topos, but not yet. On Thu, Apr 18, 2019 at 3:09 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > I only had a rough glance at your paper. But as it seems you don't > interpret directly in the infty toposes but rather in some > representing model structure. > No complaint because I don't expect otherwise. > > In any case it is quite an achievement to get universes "strongly `a > la Tarski". > > Thomas > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.