Proposed change to HoTT wiki

[Ali Caglayan]

I am proposing that we have a seperate open problems page for algebraic topology and homotopy theory in HoTT. This will allow us reduce clutter on the main open problems page and survey and collect open problems and solutions in the new page.

I suggest any results about homotopy groups and general constructions such as H-space's and (hopf constructions) be collected here as well.

Here is a link to the nforum post: https://nforum.ncatlab.org/discussion/8824/seperate-open-problems-page-for-homotopy-theory-in-hott/

Here is a link to the open problems page: https://ncatlab.org/homotopytypetheory/show/open+problems

This requires more than just moving the section in the open problems page as there are a lot of undocumented results in the last 5 years for instance. A good place to start looking for things is in the Agda and Lean (Spectral) formalisations of HoTT.

The reason I am suggesting this is because today I found a HoTT construction of the whitehead product and james construction which I totally missed from 2017: https://arxiv.org/abs/1710.10307

[Michael Shulman]

I heartily applaud the proposal to update the open problems page,
which is sorely out of date. However, I don't quite see the reason
for splitting off open problems in synthetic homotopy theory as a
separate page?

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Andrej Bauer]

There's such a thing as sections.

With kind regards,

Andrej