*[HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT@ 2018-07-28 14:26 Ali Caglayan2018-07-30 22:14 ` Michael Shulman 0 siblings, 1 reply; 2+ messages in thread From: Ali Caglayan @ 2018-07-28 14:26 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1170 bytes --] There is a preprint on the arXiv <https://arxiv.org/abs/1807.04155> about a notion of locaisation of homotopy types in HoTT. So far from what I have skimmed it seems that in the future it will be possible to calculate p-primary parts of homotopy groups. Especially since the Spectral library in Lean is having sucesses with the Serre spectral sequence, it should be too long before we see an EHP SS. Being far from an expert I am quite interested in knowing what obstacles stand in the way of formalising, say, Toda's work. I know that the Toda bracket has been resistant to defining (although I am unsure about the specifics). And I've found it quite strange that there hasn't been any siginificant development of stable homotopy theory in HoTT. What are your thoughts on this recent preprint and general thoughts about synthetic homotopy theory in HoTT? -- 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: 1429 bytes --] ^ permalink raw reply [flat|nested] 2+ messages in thread

*2018-07-28 14:26 [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT Ali CaglayanRe: [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT@ 2018-07-30 22:14 ` Michael Shulman0 siblings, 0 replies; 2+ messages in thread From: Michael Shulman @ 2018-07-30 22:14 UTC (permalink / raw) To: Ali Caglayan;+Cc:Homotopy Type Theory A quick comment about stable homotopy theory. The current HoTT approach to spectral sequences does use spectra fundamentally, so the formalization of the Serre SS involves a certain amount of theory of spectra. There is however an issue with stable homotopy theory in that (at least in "Book HoTT") there is no "strict equality". Thus, for instance, the only notion of pushout is a homotopy pushout (with specified homotopies), and similarly for smash products, which makes them rather hard to deal with; to my knowledge there is not yet a fully formalized proof that the smash product of *spaces* is coherently associative, let alone spectra. Similarly, it seems that the only available notion of spectrum is an Omega-spectrum with a sequence of spaces equivalent (not "isomorphic", which has no meaning) to each other's loop spaces -- there seems no likely possibility of "structured spectra" like symmetric spectra, orthogonal spectra, or EKMM spectra -- and even worse, the only notion of map between such spectra involves a sequence of explicitly *homotopy*-commutative squares. So the technical difficulties in dealing with all of this are an issue, although people are definitely working on it. On Sat, Jul 28, 2018 at 7:26 AM, Ali Caglayan <alizter@gmail.com> wrote: > There is a preprint on the arXiv about a notion of locaisation of homotopy > types in HoTT. So far from what I have skimmed it seems that in the future > it will be possible to calculate p-primary parts of homotopy groups. > Especially since the Spectral library in Lean is having sucesses with the > Serre spectral sequence, it should be too long before we see an EHP SS. > > Being far from an expert I am quite interested in knowing what obstacles > stand in the way of formalising, say, Toda's work. I know that the Toda > bracket has been resistant to defining (although I am unsure about the > specifics). And I've found it quite strange that there hasn't been any > siginificant development of stable homotopy theory in HoTT. > > What are your thoughts on this recent preprint and general thoughts about > synthetic homotopy theory in HoTT? > > -- > 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] 2+ messages in thread

end of thread, other threads:[~2018-07-30 22:15 UTC | newest]Thread overview:2+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-07-28 14:26 [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT Ali Caglayan 2018-07-30 22:14 ` 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).