Ordinary mathematical uses of Axiom K

Question

Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary universes of types (however many we have). Axiom K gives the following eliminator for identity types

$$K : \forall A\!:\!U. \forall x\!:\!A. \forall P\!:\!(x \equiv_A x) \rightarrow U. P(\mathrm{refl}_A x) \rightarrow \forall e\!:\!x \equiv_A x. P(e) $$

Since Axiom K is incompatible with Voevodsky's univalence principle, Homotopy Type Theory (HoTT) makes do with the weaker eliminator term J for identity types. The following question seeks to ascertain whether Axiom K has any mathematical uses that we don't (yet) know how to replace.

Question. Is there any statement $\varphi$ with the following properties?

1. $\varphi$ is a statement about ordinary mathematical structures.
2. We know how to prove $\varphi$ in MLTT+K.
3. We suspect that $\varphi$ holds in HoTT.
4. We don't know how to prove $\varphi$ in HoTT.

Clarifications.

As a first approximation to "statement about ordinary mathematical structures", I mean something that classically¹ trained analysts/algebrators/geometers would understand and investigate. For example, the statement there is a Noetherian ring that is not Artinian would definitely qualify as one about ordinary mathematical structures, while every identity type has at most one inhabitant would certainly not. Constructive reformulations of ordinary statements are perfectly fine (e.g. the Intermediate Value Theorem with appropriate "does not hover" conditions), but statements that are only interesting constructively are not (e.g. $\mathbb{N}$ has decidable equality, Markov's principle).

By MLTT+K, I mean Martin-Löf type theory, with function extensionality, axiom K, the usual sorts of inductive types you can define in Coq or Agda, and as many universe levels as you wish to take. By HoTT, I mean book HoTT, with as many universe levels as you wish to take.

An acceptable positive answer would give $\varphi$, along with a short explanation for why we suspect that it holds in HoTT, and why our proofs rely on K. If a strictly weaker variant (e.g. some existential replaced with "merely exists") of $\varphi$ already has a known proof in HoTT, that's not an issue, as long as we still suspect that $\varphi$ itself should have a proof as well.

That said, I expect the answer to be negative. I have some intuitions regarding that: e.g. the expectation that an ordinary mathematical statement will always have some ordinary first-order set-theoretic proof that we can translate to type theory, and intuitively, the type-theoretic translation of such proofs will not depend on minutiae about identity types. I am looking for more than a plausible-sounding intuitive explanation, though. An acceptable negative answer would give a mostly handwaving-free argument for why we cannot expect such a statement $\varphi$ to exist.

edit: Intent and further motivation. The intent of my question is to gauge how well we understand the possible mathematical uses of Axiom K, where understand means something like one of the following:

• We know how to eliminate this specific use of K, in that we know how to prove the conclusion in a setting where K cannot be assumed, say HoTT.
• We know that it's not possible to eliminate this specific use of K, in that we know a model, say a CwF, where the conclusion fails (of course, in such a model, as in all models of HoTT, Axiom K also fails).

Specifically, I'd like to know if there are any mathematically meaningful instances of Axiom K left which we do not understand in this sense. As a first approximation, such an instance would come from an MLTT+K proof (desideratum 2) of some $\varphi$ that that we suspect holds in HoTT, yet we don't know how to prove in HoTT (desiderata 3,4). Now, it might be that some other property $\varphi'$ has "the same ordinary mathematical meaning" as $\varphi$ in the sense given above, and yet $\varphi'$ is still provable in HoTT - indeed, it could be that for any $\varphi$ we can find such a $\varphi'$. That's not an issue, since all we need is some $\varphi$ with ordinary mathematical meaning that we think should hold in HoTT, but we don't know how to prove without K. The existence of $\varphi'$ doesn't make the original $\varphi$ any less meaningful.

¹ i.e. without ever touching upon intuitionistic or constructive mathematics; this is not a reference to some kind of mythical "education in the great classics" or to some Confucian-style elitist "traditional canon".

Answer 1

I strongly suspect that the answer to this question is "no".

In what categories can ML type theory with propositional truncations, function extensionality, and axiom $K$ (with no universes) be interpreted (assuming we don't have a version of axiom $K$ for type-level equality)? This should be the internal language of a $\Pi$-pretopos with NNO. It should be possible to take a type $T$ in ML-type theory + truncations and interpret it as a type $\ulcorner T \urcorner$ in the $\Pi$-pretopos, and to interpret element judgements $t : T$ as global elements $\ulcorner t \urcorner : 1 \to \ulcorner T \urcorner$, though I can't find a paper with the full details.

Recall that in type theory, a "set" is a type which satisfies axiom K. In other words, $Set = \left( \sum_{t \in Type} \prod_{a : t} \prod_{p : a \equiv_t a} p \equiv refl_a \right)$. Obviously we need to assume function extensionality and the existence of propositional truncations for the following result:

$Set$ is a well-pointed $\Pi$-pretopos with NNO.

This means the following:

Suppose we prove the statement $\phi$ in ML type theory plus propositional truncations, function extensionality, and $K$. Then we can find a global element $1 \to \ulcorner \phi \urcorner$ in $Set$. In other words, the statement $\phi$, relativised to Set, is true.

This statement should go through without requiring axiom $K$ at all.

Dealing with universes gets trickier. We would need to be able to internalise the notion of "universe" into our category of sets. So it's possible there are some universe-level schenanigans which prevent us from achieving our goal. Adding in the axiom of choice should get rid of these issues, however.

If your notion of "ordinary" is just "a statement about sets", then it seems pretty likely that HoTT proves all ordinary statements that ML type theory + function extensionality + propositional truncations proves, as long as we relativise these statements to be about sets rather than about types.