¬¬||🧊|| : Cubical Classics

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!

Dependency

• The Cubical Agda standard library, keeping up with the newest (maybe not publicly released yet) version.

Content

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.