[HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT

[Ali Caglayan <alizter@gmail.com>]

[-- 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 --]