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?

  • 4
    $\begingroup$ I don't know whether anyone has done it, but the way to do it would be just the same as in any other foundations (and the same as in an ordinary calculus class); basic set-level mathematics is pretty independent of foundations. $\endgroup$ – Mike Shulman Sep 6 '18 at 18:38
  • $\begingroup$ Makes sense, thanks! $\endgroup$ – user514014 Sep 7 '18 at 2:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.