This page collects desired articles in the style of a TODO list. Feel free to edit and add your own wishes. ## More on encode-decode ## 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 $\pi_1(S^1)$ and van kampen. ## Group theory ## 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. ## Directed posets, real numbers, directed colimits ## Write out a definition of a poset, a directed poset, a net, and a Cauchy net, and give a definition of the real numbers in terms of Cauchy nets in a universe, which would inevitably in the next universe. Also give a definition of an inductive system in a precategory and a directed colimit of such an inductive system.