Showing changes from revision #35 to #36:
Added | Removed | Changed
This page collects desired articles in the style of a TODO list. Feel free to edit and add your own wishes.
As of 6 June 2022, the HoTT web is regarded as deprecated. All further HoTT-related editing should happen on the main nLab web, and anyone who feels like porting an entry or two from there to here would do a great service to the community.
This method is used fruitfully in HoTT however can be a bit difficult to understand for beginners. Add some more articles detailing its use and generalisations. Specifically the proof of and van kampen.
Write out results of Higher Groups in Homotopy Type Theory. In particular outline how it can be linked with Localization in Homotopy Type Theory. Then we can finally start talking about localised cohomology.
Along the lines of Alex Simpson’s synthetic probability theory define the type of probability measures over a decidable type? and the set of random variable?s over in homotopy type theory.
Attempt to translate the results in The Dedekind Reals in Abstract Stone Duality by Andrej Bauer and Paul Taylor into homotopy type theory. Might have to work with different universe levels.