# 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 ${\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:{\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\mathrm{:}\mathrm{U}$ we have $\mathrm{\neg}\mathit{}\mathrm{(}\mathrm{\neg}\mathit{}A\mathrm{)}\mathrm{\to}A$.

###### Proof.

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

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:\mathrm{\U0001d7d0}\simeq \mathrm{\U0001d7d0}$ be the equivalence defined by $e({1}_{\mathrm{\U0001d7d0}}):\equiv {0}_{\mathrm{\U0001d7d0}}$ and $e({0}_{\mathrm{\U0001d7d0}}):\equiv {1}_{\mathrm{\U0001d7d0}}$, as in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6). Let $p:\mathrm{\U0001d7d0}=\mathrm{\U0001d7d0}$ be the path corresponding to $e$ by univalence, i.e. $p:\equiv \mathrm{\U0001d5ce\U0001d5ba}(e)$. Then we have $f(\mathrm{\U0001d7d0}):\mathrm{\neg}\mathrm{\neg}\mathrm{\U0001d7d0}\to \mathrm{\U0001d7d0}$ and

$${\mathrm{\U0001d5ba\U0001d5c9\U0001d5bd}}_{f}\left(p\right):{\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto (\mathrm{\neg}\mathrm{\neg}A\to A)}(p,f(\mathrm{\U0001d7d0}))=f(\mathrm{\U0001d7d0}).$$ |

Hence, for any $u:\mathrm{\neg}\mathrm{\neg}\mathrm{\U0001d7d0}$, we have

$$\mathrm{\U0001d5c1\U0001d5ba\U0001d5c9\U0001d5c9\U0001d5c5\U0001d5d2}({\mathrm{\U0001d5ba\U0001d5c9\U0001d5bd}}_{f}\left(p\right),u):{\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto (\mathrm{\neg}\mathrm{\neg}A\to A)}(p,f(\mathrm{\U0001d7d0}))(u)=f(\mathrm{\U0001d7d0})(u).$$ |

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

$${\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto (\mathrm{\neg}\mathrm{\neg}A\to A)}(p,f(\mathrm{\U0001d7d0}))(u)={\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto A}(p,f(\mathrm{\U0001d7d0})({\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto \mathrm{\neg}\mathrm{\neg}A}({p}^{-1},u)))$$ |

However, any two points $u,v:\mathrm{\neg}\mathrm{\neg}\mathrm{\U0001d7d0}$ are equal by function extensionality, since for any $x:\mathrm{\neg}\mathrm{\U0001d7d0}$ we have $u(x):\mathrm{\U0001d7ce}$ and thus we can derive any conclusion^{}, in particular $u(x)=v(x)$.
Thus, we have ${\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto \mathrm{\neg}\mathrm{\neg}A}({p}^{-1},u)=u$, and so from $\mathrm{\U0001d5c1\U0001d5ba\U0001d5c9\U0001d5c9\U0001d5c5\U0001d5d2}({\mathrm{\U0001d5ba\U0001d5c9\U0001d5bd}}_{f}\left(p\right),u)$ we obtain an equality

$${\mathrm{\U0001d5cd\U0001d5cb\U0001d5ba\U0001d5c7\U0001d5cc\U0001d5c9\U0001d5c8\U0001d5cb\U0001d5cd}}^{A\mapsto A}(p,f(\mathrm{\U0001d7d0})(u))=f(\mathrm{\U0001d7d0})(u).$$ |

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

$$e(f(\mathrm{\U0001d7d0})(u))=f(\mathrm{\U0001d7d0})(u).$$ | (3.2.3) |

However, we can also prove that

$$\prod _{x:\mathrm{\U0001d7d0}}\mathrm{\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}_{\mathrm{\U0001d7d0}}\ne {1}_{\mathrm{\U0001d7d0}}$ (Remark 2.12.6 (http://planetmath.org/212coproducts#Thmprermk1)).
Thus, applying (3.2.4) to $f(\mathrm{\U0001d7d0})(u)$ and (3.2.3), we obtain an element of $\mathrm{\U0001d7ce}$.
∎

###### 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 $\mathrm{\neg}\mathit{}\mathrm{\neg}\mathit{}\mathrm{\neg}\mathit{}A\mathrm{\to}\mathrm{\neg}\mathit{}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\mathrm{:}\mathrm{U}$ we have $A\mathrm{+}\mathrm{(}\mathrm{\neg}\mathit{}A\mathrm{)}$.

###### Proof.

Suppose we had $g:{\prod}_{(A:\mathcal{U})}(A+(\mathrm{\neg}A))$. We will show that then ${\prod}_{(A:\mathcal{U})}(\mathrm{\neg}\mathrm{\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:\mathrm{\neg}\mathrm{\neg}A$; we want to construct an element of $A$.

Now $g(A):A+(\mathrm{\neg}A)$, so by case analysis, we may assume either $g(A)\equiv \mathrm{\U0001d5c2\U0001d5c7\U0001d5c5}(a)$ for some $a:A$, or $g(A)\equiv \mathrm{\U0001d5c2\U0001d5c7\U0001d5cb}(w)$ for some $w:\mathrm{\neg}A$. In the first case, we have $a:A$, while in the second case we have $u(w):\mathrm{\U0001d7ce}$ 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 |