Type Classes for Mathematics in Type Theory. https://math-classes.github, 2011. ,
Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. ArXiv e-prints (2016). https://arxiv, p.9254, 1610. ,
A Monadic, Functional Implementation of Real Numbers, Mathematical Structures in Computer Science, vol.17, issue.1, pp.129-159, 2007. ,