2
$\begingroup$

According to this, Martin-Löf type theory has axiom of choice (under 'propositions as types' notion) as its theorem. That means, cubical type theory can prove the axiom of choice (its an extension of Martin-Löf type theory).

Martin-Löf is not affected by Diaconescu's theorem since it cannot prove intensionality (if for all x, f x = g x then f = g). But cubical type theory can prove intensionality. This doesn't sound right to me, I must be getting something wrong or something is broken? Cubical type theory is designed so that univalent foundations (i.e. Homotopy type theory) doesn't cause theorems to be computationally stuck. Normally, in Martin-Löf theory you take univalence as your axioms (say, postulate it in Coq or Agda) but this causes all your theorems to be computationally stuck. Instead, cubical type theory works around this problem. But it seems like Diaconescu's theorem implies cubical type theory can prove the law of excluded middle and thus it is not constructive. Now, if cubical type theory is non-constructive than Curry-Howard correspondence wouldn't hold. What is going on here, what am I missing? Is cubical type theory really non-constructive?

$\endgroup$
4
$\begingroup$

First, where you say "intensionality", you mean "extensionality" and specifically "function extensionality".

The Wikipedia page on Diaconescu's theorem uses the axiom of extensionality for sets which states that for sets $S$ and $T$, $S=T\iff(\forall x\in S.x\in T)\land(\forall x\in T.x\in S)$. It also mentions (without clear citation) that the reason Diaconescu's theorem doesn't apply to constructive type theories because they don't have an analogue of the axiom of separation.

Constructive type theories don't necessarily have a subobject classifier. Sometimes, e.g. in the Calculus of Constructions, there is a type $\mathsf{Prop}$ that is closely related to a subobject classifier. In HoTT, as described in section 3.5 of the HoTT book, we can defined a type $\mathsf{Prop}_{\mathcal U}$ via $\sum_{A:\mathcal U}\mathsf{isProp}(A)$. If we assume a propositional resizing axiom, we can define $\Omega\equiv\mathsf{Prop}_{\mathcal{U}_0}$ which will be of type $\mathcal{U}$ for any $\mathcal U$ which is a larger universe than $\mathcal{U}_0$. This behaves more like a subobject classifier. At this point the HoTT book references section 10.1.4 which asks whether the the category of sets (i.e. $0$-types in $\mathcal U$) defined in Chapter 9 is an elementary topos, i.e. whether it has a subobject classifier. $\mathsf{Prop}_{\mathcal U}$ would almost work except that it is "too big" to be of type $\mathcal U$, but propositional resizing would allow us to use $\Omega$ which is of type $\mathcal U$. The very next section presents Diaconescu's theorem in this context. It is based on the presentation of the Axiom of Choice in section 3.8.

The Axiom of Choice in section 3.8 is different from the provable type-theoretic "axiom" of choice described earlier in the book in section 1.6. One way to think about the difference between classical and constructive logic is that constructive logic introduces new logical connectives: the constructive disjunction and the constructive existential. (Edward Nelson describes it this way, it is also evident in categorical semantics for classical logic, and is also explicit at the end of section 3.7 where $P\lor Q$ and $\exists x:X.P(x)$ are defined as $||P+Q||$ and $||\sum_{x:X}P(x)||$ respectively.) So the question of which notion of existential to use when formulating the Axiom of Choice is significant. If we use the "constructive existential", i.e. the dependent sum, then we get the type-theoretic "axiom" of choice. If we use the "classical existential", i.e. the propositional truncation of the dependent sum (of a family of mere propositions), we get something that behaves like the traditional axiom of choice (and which is not provable) including leading to Diaconescu's theorem. What Diaconescu used is the usual formulation in category theory, namely that all epimorphisms are split. One could imagine formalizing this as $\prod_{A,B:\mathcal U}\prod_{f:A\to B}(\prod_{b:B}\sum_{a:A}f(a)=b)\to\sum_{g:B\to A}\prod_{a:A}f(g(a))=a$, but this is an internal statement and "all epimorphisms are split" is an external statement and there's no reason to expect the internal statement to mirror the external one (and, again, we would have to decide whether we want $\Sigma$ or $\exists$).

So, all told, the type-theoretic "axiom" of choice is not obviously the appropriate internal formulation of the axiom of choice (in fact, I think most would say it's obviously not the appropriate internal formulation), Diaconescu isn't utilizing an internal formulation anyway, and further Diaconescu was talking about elementary ($1$-)toposes while the intended models of HoTT are $(\infty,1)$-toposes. In particular, subobjects seem much less informative about higher categorical structure and indeed in the HoTT book the Axiom of Choice is limited to types with low h-level and it only talks about Diaconescu's theorem with respect to these low h-level types.

As a final note, there are Curry-Howard-style correspondences to classical proof systems, notably the $\lambda\mu$-calculus of Parigot which is given a categorical semantics in the paper I previously mentioned.

$\endgroup$
2
  • $\begingroup$ Very informative answer, every paragraph taught me new things. One question: regarding: "[...] but this is an internal statement and "all epimorphisms are split" is an external statement and there's no reason to expect the internal statement to mirror the external one." What exactly do you mean here? Why wouldn't they mirror the external statement if it is the correct formalization of the external object? $\endgroup$
    – prover
    Feb 22 '18 at 7:29
  • $\begingroup$ A statement in the internal language of a class of categories (e.g. elementary toposes) is translated to an external statement about the category being used for the semantics. This translation process is usually non-trivial. I'm saying that superficially similar symbols in a similar order in the internal language is unlikely to translate to an analogous external statement. It is simply not the case that the internal statement I gave translates to an external statement that is equivalent to "all epimorphisms split". $\endgroup$ Feb 22 '18 at 19:37

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.