My understanding is that homotopy type theory is intended as a new mathematical foundations, as is notably being written up at https://github.com/UniMath/UniMath. I am wondering whether there has been any work on the problem of doing simple calculus calculations in this setting. For example, how would you go about calculating that $\lim_{x \to \infty} \frac{1}{x} = 0$ in univalent foundations?
Homotopy type theory seems particularly well-suited to categorical constructions, so that it would not surprise me if the categorical notion of limit were easy to define. Moreover, it seems particularly suited to performing certain types of concrete calculations, like calculating homotopy groups of spheres. And finally, real numbers seem to have been implemented in the UniMath library by Voevodsky, and there is a section on them in the HoTT Book. However, the section in the book doesn't seem to calculate any specific limits, although there is a notion of limit used there in discussing Cauchy sequences and related topics.
Is it feasible to do basic calculus calculations given the state of the art of real analysis as implemented in HoTT, and has anyone done so and written it up?