3.2 Propositions as types?

Until now, we have been following the straightforward “propositions as types” philosophy described in §1.11 (http://planetmath.org/111propositionsastypes), according to which English phrases such as “there exists an $x : A$ such that $P(x)$ ” are interpreted by corresponding types such as $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$ , with the proof of a statement being regarded as judging some specific element to inhabit that type. However, we have also seen some ways in which the “logic” resulting from this reading seems unfamiliar to a classical mathematician. For instance, in Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) we saw that the statement

“If for all

x : X

there exists an

a:A(x)

such that

P(x,a)

, then there exists a function

g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}A(x)

such that for all

x : X

we have

P(x,g(x))

,”

(3.2.1)

which looks like the classical axiom of choice, is always true under this reading. This is a noteworthy, and often useful, feature of the propositions-as-types logic, but it also illustrates how significantly it differs from the classical interpretation of logic, under which the axiom of choice is not a logical truth, but an additional “axiom”.

On the other hand, we can now also show that corresponding statements looking like the classical law of double negation and law of excluded middle are incompatible with the univalence axiom.

Theorem 3.2.2.

It is not the case that for all $A:\mathcal{U}$ we have $\neg(\neg A)\to A$ .

Proof.

Recall that $\neg A\equiv(A\to\mathbf{0})$ . We also read “it is not the case that …” as the operator $\neg$ . Thus, in order to prove this statement, it suffices to assume given some $f:\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A:% \mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}(\neg\neg A\to A)$ and construct an element of $\mathbf{0}$ .

The idea of the following proof is to observe that $f$ , like any function in type theory, is “continuous”. By univalence, this implies that $f$ is natural with respect to equivalences of types. From this, and a fixed-point-free autoequivalence, we will be able to extract a contradiction.

Let $e:\mathbf{2}\simeq\mathbf{2}$ be the equivalence defined by $e({1_{\mathbf{2}}}):\!\!\equiv{0_{\mathbf{2}}}$ and $e({0_{\mathbf{2}}}):\!\!\equiv{1_{\mathbf{2}}}$ , as in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6). Let $p:\mathbf{2}=\mathbf{2}$ be the path corresponding to $e$ by univalence, i.e. $p:\!\!\equiv\mathsf{ua}(e)$ . Then we have $f(\mathbf{2}):\neg\neg\mathbf{2}\to\mathbf{2}$ and

\mathsf{apd}_{f}\mathopen{}\left(p\right)\mathclose{}:\mathsf{transport}^{A% \mapsto(\neg\neg A\to A)}(p,f(\mathbf{2}))=f(\mathbf{2}).

Hence, for any $u:\neg\neg\mathbf{2}$ , we have

\mathsf{happly}(\mathsf{apd}_{f}\mathopen{}\left(p\right)\mathclose{},u):% \mathsf{transport}^{A\mapsto(\neg\neg A\to A)}(p,f(\mathbf{2}))(u)=f(\mathbf{2% })(u).

Now by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), transporting $f(\mathbf{2}):\neg\neg\mathbf{2}\to\mathbf{2}$ along $p$ in the type family ${A\mapsto(\neg\neg A\to A)}$ is equal to the function which transports its argument along $\mathord{{p}^{-1}}$ in the type family $A\mapsto\neg\neg A$ , applies $f(\mathbf{2})$ , then transports the result along $p$ in the type family $A\mapsto A$ :

\mathsf{transport}^{A\mapsto(\neg\neg A\to A)}(p,f(\mathbf{2}))(u)=\mathsf{% transport}^{A\mapsto A}(p,f(\mathbf{2})(\mathsf{transport}^{A\mapsto\neg\neg A% }(\mathord{{p}^{-1}},u)))

However, any two points $u,v:\neg\neg\mathbf{2}$ are equal by function extensionality, since for any $x:\neg\mathbf{2}$ we have $u(x):\mathbf{0}$ and thus we can derive any conclusion, in particular $u(x)=v(x)$ . Thus, we have $\mathsf{transport}^{A\mapsto\neg\neg A}(\mathord{{p}^{-1}},u)=u$ , and so from $\mathsf{happly}(\mathsf{apd}_{f}\mathopen{}\left(p\right)\mathclose{},u)$ we obtain an equality

\mathsf{transport}^{A\mapsto A}(p,f(\mathbf{2})(u))=f(\mathbf{2})(u).

Finally, as discussed in §2.10 (http://planetmath.org/210universesandtheunivalenceaxiom), transporting in the type family $A\mapsto A$ along the path $p\equiv\mathsf{ua}(e)$ is equivalent to applying the equivalence $e$ ; thus we have

e(f(\mathbf{2})(u))=f(\mathbf{2})(u).

(3.2.3)

However, we can also prove that

\mathchoice{\prod_{x:\mathbf{2}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbf{2% })}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}% {\mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod% _{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:% \mathbf{2})}}}\neg(e(x)=x).

(3.2.4)

This follows from a case analysis on $x$ : both cases are immediate from the definition of $e$ and the fact that ${0_{\mathbf{2}}}\neq{1_{\mathbf{2}}}$ (Remark 2.12.6 (http://planetmath.org/212coproducts#Thmprermk1)). Thus, applying (3.2.4) to $f(\mathbf{2})(u)$ and (3.2.3), we obtain an element of $\mathbf{0}$ . ∎

Remark 3.2.5.

In particular, this implies that there can be no Hilbert-style “choice operator” which selects an element of every nonempty type. The point is that no such operator can be natural, and under the univalence axiom, all functions acting on types must be natural with respect to equivalences.

Remark 3.2.6.

It is, however, still the case that $\neg\neg\neg A\to\neg A$ for any $A$ ; see http://planetmath.org/node/87564Exercise 1.11.

Corollary 3.2.7.

It is not the case that for all $A:\mathcal{U}$ we have $A+(\neg A)$ .

Proof.

Suppose we had $g:\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A:% \mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:% \mathcal{U})}}{\prod_{(A:\mathcal{U})}}}(A+(\neg A))$ . We will show that then $\mathchoice{\prod_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(A:\mathcal% {U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U% })}}}{\mathchoice{{\textstyle\prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}% }{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(A:\mathcal{U})}}}{\prod_{(A:\mathcal{U})}}{\prod_{(A:\mathcal{U})}}{% \prod_{(A:\mathcal{U})}}}(\neg\neg A\to A)$ , so that we can apply Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1). Thus, suppose $A:\mathcal{U}$ and $u:\neg\neg A$ ; we want to construct an element of $A$ .

Now $g(A):A+(\neg A)$ , so by case analysis, we may assume either $g(A)\equiv{\mathsf{inl}}(a)$ for some $a : A$ , or $g(A)\equiv{\mathsf{inr}}(w)$ for some $w:\neg A$ . In the first case, we have $a : A$ , while in the second case we have $u(w):\mathbf{0}$ and so we can obtain anything we wish (such as $A$ ). Thus, in both cases we have an element of $A$ , as desired. ∎

Thus, if we want to assume the univalence axiom (which, of course, we do) and still leave ourselves the option of classical reasoning (which is also desirable), we cannot use the unmodified propositions-as-types principle to interpret all informal mathematical statements into type theory, since then the law of excluded middle would be false. However, neither do we want to discard propositions-as-types entirely, because of its many good properties (such as simplicity, constructivity, and computability). We now discuss a modification of propositions-as-types which resolves these problems; in §3.10 (http://planetmath.org/310whenarepropositionstruncated) we will return to the question of which logic to use when.

Title	3.2 Propositions as types?
\metatable