* Re: [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT
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
0 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