This page collects desired articles in the style of a TODO list. Feel free to edit and add your own wishes. ## The type theory navigation list ## The [[type theory]] navigation list is terrible as it stands. Eventually these articles will need to be written and incorporated into the wiki. Right now they seem lost. ## 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.