From program halts in the tale, towards program only Übermensch is able to run.
The aim of cubical-classics library is to formalize classical mathematics using cubical type theory.
Though still a baby project at present, I hope someday it will have some important ideas of modern mathematics eventually.
We are open to advices and contributions!
- The Cubical Agda standard library, keeping up with the newest (maybe not publicly released yet) version.
A glimpse of things that have been formalized:
- Results concerning classical axioms, especially Diaconescu's theorem;
- Classical impredicative powerset, setting up a structural set theory;
- Topological spaces, compactness, Hausdorff axiom and metric spaces;
- Construction of classical Dedekind real, and it is a complete Archimedean ordered field;
- Basic theorems of real number including monotone convergence theorem, Heine-Borel theorem, Bolzano-Weierstrass theorem and the convergence of Cauchy sequences;
- Intermediate value theorem of continuous real functions.