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.