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. ## Probability theory ## Along the lines of Alex Simpson's [synthetic probability theory](http://tobiasfritz.science/2019/cps_workshop/slides/simpson.pdf) define the type of [[probability measure]]s $\mathcal{M}_1(A)$ over a [[decidable type]] $A$ and the set of [[random variable]]s $RV(A)$ over $A$ in homotopy type theory. ## Solèr's theorem and the category of Hilbert spaces ## Define the terms used to define and prove [[Solèr's theorem]] in a constructive and predicative manner, and the terms used in the article [[HilbR]] to define the category of Hilbert spaces over the real numbers in a constructive and predicative manner. ## Order theory ## Write out a definition of a countably complete directed poset. Define partial function classifiers as a higher inductive-inductive type, as the free countably complete directed poset, and Sierpinski space as the partial function classifier on the unit type.