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. ## Elementary algebra ## We work in the rational numbers here, to sidestep any issues with constructing the real numbers. * [[field (ring theory)]] * [[function]] * [[function algebra]] * [[constant function]] * [[identity function]] * [[linear function]] * [[affine function]] * [[quadratic function]] * [[cubic function]] * [[polynomial function]] * [[rational root theorem]] * [[partial function]] * [[category of partial functions]] * [[rational function]] Fred Richman's [Algebraic functions, calculus style](https://web.archive.org/web/20130605213603/http://math.fau.edu/richman/Docs/Oily.pdf) for reference ## 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. ## Abstract Stone Duality ## Attempt to translate the results in [The Dedekind Reals in Abstract Stone Duality](https://www.paultaylor.eu/ASD/dedras/index.html) by Andrej Bauer and Paul Taylor into homotopy type theory. Might have to work with different universe levels.