This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath


Authors: Catherine Lelay

This Coq library provides a formalization of real numbers built using Dedekind cuts.

It builds upon V. Voevodsky’s Foundations library, available on http://arxiv.org/abs/1401.0053.

For any question about this library, send an email to Catherine Lelay.