* [HoTT] All (∞,1)-toposes have strict univalent universes @ 2019-04-16 12:06 Ali Caglayan 2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory 0 siblings, 1 reply; 5+ messages in thread From: Ali Caglayan @ 2019-04-16 12:06 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] All (∞,1)-toposes have strict univalent universes 2019-04-16 12:06 [HoTT] All (∞,1)-toposes have strict univalent universes Ali Caglayan @ 2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory 2019-04-17 23:44 ` Michael Shulman 0 siblings, 1 reply; 5+ messages in thread From: 'Martin Escardo' via Homotopy Type Theory @ 2019-04-17 22:59 UTC (permalink / raw) To: Ali Caglayan, Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] All (∞,1)-toposes have strict univalent universes 2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory @ 2019-04-17 23:44 ` Michael Shulman 2019-04-18 10:09 ` [HoTT] All (???,1)-toposes " Thomas Streicher 0 siblings, 1 reply; 5+ messages in thread From: Michael Shulman @ 2019-04-17 23:44 UTC (permalink / raw) To: Martin Escardo; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] All (???,1)-toposes have strict univalent universes 2019-04-17 23:44 ` Michael Shulman @ 2019-04-18 10:09 ` Thomas Streicher 2019-04-18 10:16 ` Michael Shulman 0 siblings, 1 reply; 5+ messages in thread From: Thomas Streicher @ 2019-04-18 10:09 UTC (permalink / raw) To: Michael Shulman; +Cc: Martin Escardo, Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [HoTT] All (???,1)-toposes have strict univalent universes 2019-04-18 10:09 ` [HoTT] All (???,1)-toposes " Thomas Streicher @ 2019-04-18 10:16 ` Michael Shulman 0 siblings, 0 replies; 5+ messages in thread From: Michael Shulman @ 2019-04-18 10:16 UTC (permalink / raw) To: Thomas Streicher; +Cc: Martin Escardo, Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2019-04-18 10:17 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2019-04-16 12:06 [HoTT] All (∞,1)-toposes have strict univalent universes Ali Caglayan 2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory 2019-04-17 23:44 ` Michael Shulman 2019-04-18 10:09 ` [HoTT] All (???,1)-toposes " Thomas Streicher 2019-04-18 10:16 ` Michael Shulman
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).