1
$\begingroup$

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".

$\endgroup$
5
  • $\begingroup$ What's the purpose of your condition 3? It seems to me that a statement $\varphi$ satisfying only 1, 2, 4 would make an even stronger claim about the un-replaceability of axiom K. $\endgroup$ Nov 16, 2021 at 6:31
  • $\begingroup$ @MikeShulman There are many ways to formalize a given informal mathematical statement in type theory (think e.g. propositions-as-types vs. propositions-as-some-types) that a classical mathematician would not recognize as meaningfully different. Condition 3 is meant to rule out "technical solutions" where there are two formalizations φ and φ', and the logical equivalence of φ and φ' somehow relies on Axiom K. 1/2 $\endgroup$
    – Z. A. K.
    Nov 16, 2021 at 10:25
  • $\begingroup$ In that case, it might be that φ is provable only in MLTT+K, while φ' is provable without K, but the use of Axiom K is in some sense purely logical, not an ordinary mathematical use of the sort I'm interested in. The idea is that such a φ would satisfy conditions 1,2,4, but not 3. 2/2 $\endgroup$
    – Z. A. K.
    Nov 16, 2021 at 10:31
  • $\begingroup$ @MikeShulman Probably a better, more succinct answer than the one I gave above: condition 3 is meant to rule out cases where someone "bakes" Axiom K into the statement φ itself - if they did that, they'd have no reason to suspect that φ should hold in HoTT as well. $\endgroup$
    – Z. A. K.
    Nov 16, 2021 at 10:38
  • 1
    $\begingroup$ Hmm... so, something like the strong form of the axiom of choice that's inconsistent with univalence, but nevertheless "appears" to be a statement "only about sets"? $\endgroup$ Nov 16, 2021 at 18:03

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for writing this up! Amusingly, your answer describes, almost exactly, the original circumstances that prompted me to ask the question. A few weeks ago I was reading Moerdijk-Palmgren on $\Pi$W-pretopoi: I had the thought that what you summarized as "This statement should go through without requiring axiom K at all" should probably hold. I tried, but repeatedly failed to convince myself of that, and in fact I still don't see why it should hold, and am no longer sure it does. In any case, that's a different, albeit related question (one that I intend to ask on this site at some point). $\endgroup$
    – Z. A. K.
    Nov 19, 2021 at 15:46
  • $\begingroup$ To explain why the current question is different, I added an "Intent/Motivation" section to the question body (see also my Nov 16 discussion with Mike Shulman above). $\endgroup$
    – Z. A. K.
    Nov 19, 2021 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.