Consider two developments in dependent type theory:
- Lean’s
mathliblibrary (as well many other ITP libraries) is unashamedly fully classical. There is no hesitation to use the law of excluded middle (LEM) or the axiom of choice (AC). And there is no interest in constructive definitions or theorems when there is an easier classical one. - Libraries based on homotopy type theory (HoTT) are unashamedly fully univalent. They use the Univalence axiom (UA) and higher-inductive types (HITs) whenever it makes sense to prove results and build definitions.
Contrarily to popular opinion these approaches aren’t mutually exclusive. Univalence is compatible with classical reasoning (with some caveats I’ll mention).
What would an unashamedly fully univalent and fully classical library of mathematics look like? In particular, the library would be just as classical as mathlib, but heavily use UA and HITs.
I’m imagining something like mathlib but built on top of one of the following:
- Lean reworked to support HoTT or cubical type theory (and axioms LEM/AC)
- A merger of Lean and Arend taking parts from both
- Arend, but with axioms for LEM and AC
- Coq with axioms LEM, AC, UA, and HITs
- Any of the other cubical type theories with axioms for LEM and AC.
How would an ITP needed to support such a library differ from Lean’s design choices, and what would be the consequences? Conversely, what new possibilities would arise?
Here are some considerations to think about.
- Lean has some features which conflict with UA. It might be that some such Lean features would be sorely missed, or maybe UA would provide good replacements.
- The Lean version of LEM would remain the same but the Lean version of AC would have to be weakened. One can only state the proposition that there exists a choice function. One can’t use it in a definition per se. For example, one can’t construct a function which takes a vector space to a basis. They can only prove a proposition that such a function exists.
- However, UA gives unique choice, so for example one can construct (non-constructively) a true function which takes a vector space to its dimension. (And one can even use the existence of a basis function mentioned above in the definition.)
- I often hear UA is a way to make transfer of things easier between isomorphic types. Would this be true in practice?
- Lean’s quotients supposedly help avoid “setoid hell”? Would we be back to setoid hell?
- Lean has the ability to work with computable definitions and non-constructive proofs together. Would baseing constructions like quotients on UA make it easier to have computable definitions for common mathematical objects?
- Most of the Lean mathlib theorems are about sets (in the HoTT sense), so those theorems would remain the same but with the condition that one is talking about sets instead of types (which at least in Arend is easy to express in the type theory).
- On the other hand, theorems about arbitrary sets and types would look different now since the type of sets and the type of all small types would be a higher type.
- A complaint of HoTT is that it is (by definition) synthetic, but if one gives a classical definition of homotopy (through topological spaces) and connects it to the synthetic one then one can prove results in homotopy theory using a combination of both classical and synthetic approaches. Is this feasible? Interesting?
Note, this is purely a mental exercise. I’m not proposing someone build this library. But at the same time, it does get discussed from time to time so it would be nice to get thoughts on what it would look like.
