Paper Explanations: Formalising Real Numbers in Homotopy Type Theory + Partiality, Revisited
In the summer of 2017, as part of the work I did in my master’s program, I wrote summaries on two relatively-recent papers which interested me:
-“Formalising Real Numbers in Homotopy Type Theory”: This paper winds up formalizing the reals in HoTT fairly elegantly as the Cauchy completion of the rational numbers, and as a pleasant side-effect, it also demonstrates that the Cauchy completion of pre-metric spaces forms a monad. I threw in a bit of explanation about monads at the beginning, so this is probably the closest you’ll ever get to an infamous “monad tutorial” written by me.
-“Partiality Revisited”: This one winds up leveraging a particularly clever higher-inductive type to be able to economically express partial (possibly non-terminating) functions, which allows for a nice definition for semi-decidability in HoTT.
Despite their seemingly separate topics, the two papers above actually mesh very well, since together, they allow for the demonstration of a semi-decision procedure for a “closeness” relation on the reals.
As a fun bonus, I also illustrate the definition and application of the double-negation monad in HoTT.