Prospects for reverse mathematics in Homotopy Type Theory

Question

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include

• Subsystems of Second Order Arithmetic (SOSOA). Theorems expressible in second order arithmetic are compared over $\mathsf{RCA}_0$ (which is roughly the theory of computable sets of natural numbers).

• Constructive Reverse Mathematics. Bridges and others use Bishop-style constructive mathematics as a base theory to compare various nonn-constructive principles.

Here are my questions.

1. Would it be possible to do reverse mathematics over Homotopy Type Theory (HoTT)?

2. Would HoTT make for a good base theory (roughly corresponding to computable objects in mathematics)? My understanding is that HoTT is a constructive theory, this makes me believe the answer is yes.

3. Would the univalence axiom need to be removed from the base theory? My understanding is that the univalence axiom is incompatible with the law of excluded middle. This would be problematic.

4. Would the results be similar to those in Constructive Reverse Mathematics? (Would they be exactly the same?)

5. Would computability theoretic ideas be of use as they are in SOSOA reverse mathematics? Computability theorists are drawn to SOSOA because of its computability theoretic nature.

6. Would the computer implementations of HoTT, in say Coq, be helpful in proving reverse-mathematics-like results. It would be nice to be able to do reverse mathematics with the "safety net" of a proof checker.

7. Has reverse mathematics in HoTT been done already in any sense (formally or informally)?

Note: There may be some relationship with this question: Forcing in homotopy type theory

Answer 1

Before I attempt to address your specific questions, let me give a thought provoking non-answer:

Reverse mathematics is impossible (and irrelevant) in HoTT!

This is because HoTT fully supports proof-relevant mathematics, so when you refer to a theorem you necessarily refer to a proof of that theorem. The question whether the hypotheses are necessary doesn't make sense in this context since the hypotheses are part of the theorem itself!

Now that your thoughts have been provoked, let me amend the above statement:

HoTT is not the end of reverse mathematics!

Actually, it just makes the reverse (and constructive) mathematics questions even more obvious. The most fundamental reason why reverse mathematics exists is the incredible power of the existential quantifier. In HoTT, that is immediately obvious. A plain existential statement is interpreted as a dependent sum type in HoTT: "$\sum_{x:A} P(x)$ is inhabited" is the right way to say that "there is an $x$ of type $A$ such that $P(x)$." By definition, every inhabitant $x:A$ of this type is equipped with a justification of $P(x)$. To get the usual existential quantifier, one must truncate $\sum_{x:A} P(x)$ to a proposition. This raises the question: can this truncation be reversed? What are the necessary hypotheses to reverse this truncation? This is what reverse mathematics questions get turned into when translated into the language of HoTT. Note how "mathematical" the reverse mathematics question has become! This is no surprise to practicing reverse mathematicians but it is very interesting how reverse mathematics becomes less mythical in this context.

---

I will now add what I know about each of your questions. Since I'm still learning about HoTT, these answers are far from complete or definitive. I hope that experts will chime in at some point.

1. The above sort of addresses this question. An additional difficulty is that it seems that there is still some work to be done in understanding models of HoTT. The soundness and completeness theorems obtained by Awodey & Warren and Gambino & Garner are almost there but Awodey points out some subtle issues. I don't know if these issues are problematic enough to make it difficult to establish non-provability results for HoTT.

2. HoTT is perhaps too strong for use as a base system for classical reverse mathematics. The reason is basically the same as why ZF is often too strong for that purpose. Note, however that even ZF is not completely useless. For example, as witnessed by a great deal of literature, ZF is a perfectly fine base theory for the analysis of choice principles. HoTT is more promising as a base system for constructive reverse mathematics but the constructivity of the univalence axiom is currently an open problem.

3. I don't think the univalence axiom is that problematic. The law of excluded middle always clashes with the propositions-as-types interpretation. The correct way to formulate the law of excluded middle in HoTT is to restrict it to propositions — types with at most one element. This version of the law of excluded middle does not clash with univalence and captures all of the normal uses.

4. I don't think anyone has addressed the question whether HoTT is a conservative extension of BISH (say) or how far it is from being a conservative extension.

5. It's difficult to make a comparison. The base system RCA₀ was explicitly designed to capture basic computability theory. HoTT wasn't designed that way but other aspects of computability were important design components.

6. I don't see much gain in using proof assistants for reverse mathematics but I might be nearsighted.

7. Yes, some additional axioms such as propositional resizing, the law of excluded middle, and the axiom of choice have been analyzed to some extent. HoTT is so young that very little of this has been done yet.

Answer 2

At present, homotopy type theory is purported to be the internal language (i.e. syntax) of $(\infty,1)$-topoi. That univalence is an axiom is to say that there is a class of higher topoi that satisfy univalence and a class of higher topoi that do not. For instance, the topos of sets, together with trivial higher morphisms, do not satisfy univalence.

Suppose we wish to pursue the reverse mathematics of any theorem that has been proven in homotopy type theory. Take any theorem, say, like in my comment, that the fundamental group of the circle is the integers. In this paper by Shulman and Licata, they mention that univalence is required to prove this theorem. As I see it, the circle in the topos of sets, where univalence does not hold, is actually just the singleton set. Every path and higher path is trivial. Hence the fundamental group of the circle, in the model of the topos of sets, is trivial.

A reverse mathematician interested to study the strength of this topogical result would want to see how much of univalence is required. Is there a higher topos in which univalence fails yet the fundamental group of the circle is still the integers? Can we characterize those higher topoi in which the fundamental group of the circle is the integers? Can we characterize these topoi syntactically?