B. Spitters and E. Van-der-weegen, Type Classes for Mathematics in Type Theory. https://math-classes.github, 2011.

T. Altenkirch, N. A. Danielsson, N. Kraus, and . Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. ArXiv e-prints (2016). https://arxiv, p.9254, 1610.

O. Russell and . Connor, A Monadic, Functional Implementation of Real Numbers, Mathematical Structures in Computer Science, vol.17, issue.1, pp.129-159, 2007.