logic.tex

\chapter{Sets and logic}
\label{cha:logic}

Type theory, formal or informal, is a collection of rules for manipulating types and their elements.
But when writing mathematics informally in natural language, we generally use familiar words, particularly logical connectives such as ``and'' and ``or'', and logical quantifiers such as ``for all'' and ``there exists''.
In contrast to set theory, type theory offers us more than one way to regard these English phrases as operations on types.
This potential ambiguity needs to be resolved, by setting out local or global conventions, by introducing new annotations to informal mathematics, or both.
This requires some getting used to, but is offset by the fact that because type theory permits this finer analysis of logic, we can represent mathematics more faithfully, with fewer ``abuses of language'' than in set-theoretic foundations.
In this chapter we will explain the issues involved, and justify the choices we have made.

\section{Sets and \texorpdfstring{$n$}{n}-types}
\label{sec:basics-sets}

\index{set|(defstyle}%

In order to explain the connection between the logic of type theory and the logic of set theory, it is helpful to have a notion of \emph{set} in type theory.
While types in general behave like spaces or higher groupoids, there is a subclass of them that behave more like the sets in a traditional set-theoretic system.
Categorically, we may consider \emph{discrete} groupoids, which are determined by a set of objects and only identity morphisms as higher morphisms; while topologically, we may consider spaces having the discrete topology.\index{discrete!space}
More generally, we may consider groupoids or spaces that are \emph{equivalent} to ones of this sort; since everything we do in type theory is up to homotopy, we can't expect to tell the difference.

Intuitively, we would expect a type to ``be a set'' in this sense if it has no higher homotopical information: any two parallel paths are equal (up to homotopy), and similarly for parallel higher paths at all dimensions.
Fortunately, because everything in homotopy type theory is automatically functorial/continuous,
\index{continuity of functions in type theory@``continuity'' of functions in type theory}%
\index{functoriality of functions in type theory@``functoriality'' of functions in type theory}%
it turns out to be sufficient to ask this at the bottom level.

\begin{defn}\label{defn:set}
  A type $A$ is a \define{set}
  if for all $x,y:A$ and all $p,q:x=y$, we have $p=q$.
\end{defn}

More precisely, the proposition $\isset(A)$ is defined to be the type
\[ \isset(A) \defeq \prd{x,y:A}{p,q:x=y} (p=q). \]

As mentioned in \cref{sec:types-vs-sets},
the sets in homotopy type theory are not like the sets in ZF set theory, in that there is no global ``membership predicate'' $\in$.
They are more like the sets used in structural mathematics and in category theory, whose elements are ``abstract points'' to which we give structure with functions and relations.
This is all we need in order to use them as a foundational system for most set-based mathematics; we will see some examples in \cref{cha:set-math}.

Which types are sets?
In \cref{cha:hlevels} we will study a more general form of this question in depth, but for now we can observe some easy examples.

\begin{eg}\label{eg:isset-unit}
  The type \unit is a set.
  For by \cref{thm:path-unit}, for any $x,y:\unit$ the type $(x=y)$ is equivalent to \unit.
  Since any two elements of \unit are equal, this implies that any two elements of $x=y$ are equal.
\end{eg}

\begin{eg}\label{eg:isset-empty}
  The type $\emptyt$ is a set, for given any $x,y:\emptyt$ we may deduce anything we like, by the induction principle of $\emptyt$.
\end{eg}

\begin{eg}\label{thm:nat-set}
  The type \nat of natural numbers is also a set.
  This follows from \cref{thm:path-nat}, since all equality types $\id[\nat]xy$ are equivalent to either \unit or \emptyt, and any two inhabitants of \unit or \emptyt are equal.
  We will see another proof of this fact in \cref{cha:hlevels}.
\end{eg}

Most of the type forming operations we have considered so far also preserve sets.

\begin{eg}\label{thm:isset-prod}
  If $A$ and $B$ are sets, then so is $A\times B$.
  For given $x,y:A\times B$ and $p,q:x=y$, by \cref{thm:path-prod} we have $p= \pairpath(\projpath1(p),\projpath2(p))$ and $q= \pairpath(\projpath1(q),\projpath2(q))$.
  But $\projpath1(p)=\projpath1(q)$ since $A$ is a set, and $\projpath2(p)=\projpath2(q)$ since $B$ is a set; hence $p=q$.

  Similarly, if $A$ is a set and $B:A\to\type$ is such that each $B(x)$ is a set, then $\sm{x:A} B(x)$ is a set.
\end{eg}

\begin{eg}\label{thm:isset-forall}
  If $A$ is \emph{any} type and $B:A\to \type$ is such that each $B(x)$ is a set, then the type $\prd{x:A} B(x)$ is a set.
  For suppose $f,g:\prd{x:A} B(x)$ and $p,q:f=g$.
  By function extensionality, we have
  %
  \begin{equation*}
    p = {\funext (x \mapsto \happly(p,x))}
    \quad\text{and}\quad
    q = {\funext (x \mapsto \happly(q,x))}.
  \end{equation*}
  %
  But for any $x:A$, we have
  %
  \begin{equation*}
   \happly(p,x):f(x)=g(x)
   \qquad\text{and}\qquad
   \happly(q,x):f(x)=g(x),
  \end{equation*}
  %
  so since $B(x)$ is a set we have $\happly(p,x) = \happly(q,x)$.
  Now using function extensionality again, the dependent functions $(x \mapsto \happly(p,x))$ and $(x \mapsto \happly(q,x))$ are equal, and hence (applying $\apfunc{\funext}$) so are~$p$ and~$q$.
\end{eg}

For more examples, see \cref{ex:isset-coprod,ex:isset-sigma}.  For a more systematic investigation of the subsystem (category) of all sets in homotopy type theory, see~\cref{cha:set-math}.

\index{n-type@$n$-type|(}%

Sets are just the first rung on a ladder of what are called \emph{homotopy $n$-types}.
The next rung consists of \emph{$1$-types}, which are analogous to $1$-groupoids in category theory.
The defining property of a set (which we may also call a \emph{$0$-type}) is that it has no non-trivial paths.
Similarly, the defining property of a $1$-type is that it has no non-trivial paths between paths:

\begin{defn}\label{defn:1type}
  A type $A$ is a \define{1-type}
  \indexdef{1-type}%
  if for all $x,y:A$ and $p,q:x=y$ and $r,s:p=q$, we have $r=s$.
\end{defn}

Similarly, we can define $2$-types, $3$-types, and so on.
We will define the general notion of $n$-type inductively in \cref{cha:hlevels}, and study the relationships between $n$-types for different values of $n$.

However, for now it is useful to have two facts in mind.
First, the levels are upward-closed: if $A$ is an $n$-type then $A$ is an $(n+1)$-type.
For example:
%%  will make precise the sense in which this
%% ``suffices for all higher levels'', but as an example, we observe that
%% it suffices for the next level up.

\begin{lem}\label{thm:isset-is1type}
  If $A$ is a set (that is, $\isset(A)$ is inhabited), then $A$ is a 1-type.
\end{lem}
\begin{proof}
  Suppose $f:\isset(A)$; then for any $x,y:A$ and $p,q:x=y$ we have $f(x,y,p,q):p=q$.
  Fix $x$, $y$, and $p$, and define $g: \prd{q:x=y} (p=q)$ by $g(q) \defeq f (x,y,p,q)$.
  Then for any $r:q=q'$, we have $\apdfunc{g}(r) : \trans{r}{g(q)} = g(q')$.
  By \cref{cor:transport-path-prepost}, therefore, we have $g(q) \ct r = g(q')$.

  In particular, suppose given $x,y,p,q$ and $r,s:p=q$, as in \cref{defn:1type}, and define $g$ as above.
  Then $g(p) \ct r = g(q)$ and also $g(p) \ct s = g(q)$, hence by cancellation $r=s$.
\end{proof}

Second, this stratification of types by level is not degenerate, in the
sense that not all types are sets:

\begin{eg}\label{thm:type-is-not-a-set}
  \index{type!universe}%
  The universe \type is not a set.
  To prove this, it suffices to exhibit a type $A$ and a path $p:A=A$ which is not equal to $\refl A$.
  Take $A=\bool$, and let $f:A\to A$ be defined by $f(\bfalse)\defeq \btrue$ and $f(\btrue)\defeq \bfalse$.
  Then $f(f(x))=x$ for all $x$ (by an easy case analysis), so $f$ is an equivalence.
  Hence, by univalence, $f$ gives rise to a path $p:A=A$.

  If $p$ were equal to $\refl A$, then (again by univalence) $f$ would equal the identity function of $A$.
  But this would imply that $\bfalse=\btrue$, contradicting \cref{rmk:true-neq-false}.
\end{eg}

In \cref{cha:hits,cha:homotopy} we will show that for any $n$, there are types which are not $n$-types.

Note that $A$ is a 1-type exactly when for any $x,y:A$, the identity type $\id[A]xy$ is a set.
(Thus, \cref{thm:isset-is1type} could equivalently be read as saying that the identity types of a set are also sets.)
This will be the basis of the recursive definition of $n$-types we will give in \cref{cha:hlevels}.

We can also extend this characterization ``downwards'' from sets.
That is, a type $A$ is a set just when for any $x,y:A$, any two elements of $\id[A]xy$ are equal.
Since sets are equivalently 0-types, it is natural to call a type a \emph{$(-1)$-type} if it has this latter property (any two elements of it are equal).
Such types may be regarded as \emph{propositions in a narrow sense}, and their study is just what is usually called ``logic''; it will occupy us for the rest of this chapter.

\index{n-type@$n$-type|)}%
\index{set|)}%

\section{Propositions as types?}
\label{subsec:pat?}

\index{proposition!as types|(}%
\index{logic!constructive vs classical|(}%
\index{anger|(}%
Until now, we have been following the straightforward ``propositions as types'' philosophy described in \cref{sec:pat}, according to which English phrases such as ``there exists an $x:A$ such that $P(x)$'' are interpreted by corresponding types such as $\sm{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 \cref{thm:ttac} we saw that the statement
\index{axiom!of choice!type-theoretic}%
\begin{equation}\label{eq:english-ac}
  \parbox{\textwidth-2cm}{``If for all $x:X$ there exists an $a:A(x)$ such that $P(x,a)$, then there exists a function $g:\prd{x:X} A(x)$ such that for all $x:X$ we have $P(x,g(x))$'',}
\end{equation}
which looks like the classical\index{mathematics!classical} \emph{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 \emph{law of double negation} and \emph{law of excluded middle} are incompatible with the univalence axiom.
\index{univalence axiom}%

\begin{thm}\label{thm:not-dneg}
  \index{double negation, law of}%
  It is not the case that for all $A:\UU$ we have $\neg(\neg A) \to A$.
\end{thm}
\begin{proof}
  Recall that $\neg A \jdeq (A\to\emptyt)$.
  We also read ``it is not the case that \dots'' as the operator $\neg$.
  Thus, in order to prove this statement, it suffices to assume given some $f:\prd{A:\UU} (\neg\neg A \to A)$ and construct an element of \emptyt.

  The idea of the following proof is to observe that $f$, like any function in type theory, is ``continuous''.
  \index{continuity of functions in type theory@``continuity'' of functions in type theory}%
  \index{functoriality of functions in type theory@``functoriality'' of functions in type theory}%
  By univalence, this implies that $f$ is \emph{natural} with respect to equivalences of types.
  From this, and a fixed-point-free autoequivalence\index{automorphism!fixed-point-free}, we will be able to extract a contradiction.

  Let $e:\eqv\bool\bool$ be the equivalence defined by $e(\btrue)\defeq\bfalse$ and $e(\bfalse)\defeq\btrue$, as in \cref{thm:type-is-not-a-set}.
  Let $p:\bool=\bool$ be the path corresponding to $e$ by univalence, i.e.\ $p\defeq \ua(e)$.
  Then we have $f(\bool) : \neg\neg\bool \to\bool$ and
  \[\apd f p : \transfib{A\mapsto (\neg\neg A \to A)}{p}{f(\bool)} = f(\bool).\]
  Hence, for any $u:\neg\neg\bool$, we have
  \[\happly(\apd f p,u) : \transfib{A\mapsto (\neg\neg A \to A)}{p}{f(\bool)}(u) = f(\bool)(u).\]

  Now by~\eqref{eq:transport-arrow}, transporting $f(\bool):\neg\neg\bool\to\bool$ along $p$ in the type family ${A\mapsto (\neg\neg A \to A)}$ is equal to the function which transports its argument along $\opp p$ in the type family $A\mapsto \neg\neg A$, applies $f(\bool)$, then transports the result along $p$ in the type family $A\mapsto A$:
  \begin{narrowmultline*}
    \transfib{A\mapsto (\neg\neg A \to A)}{p}{f(\bool)}(u) =
    \narrowbreak
    \transfib{A\mapsto A}{p}{f(\bool) (\transfib{A\mapsto \neg\neg
        A}{\opp{p}}{u})}.
  \end{narrowmultline*}
  %
  However, any two points $u,v:\neg\neg\bool$ are equal by function extensionality, since for any $x:\neg\bool$ we have $u(x):\emptyt$ and thus we can derive any conclusion, in particular $u(x)=v(x)$.
  Thus, we have $\transfib{A\mapsto \neg\neg A}{\opp{p}}{u} = u$, and so from $\happly(\apd f p,u)$ we obtain an equality
  \[ \transfib{A\mapsto A}{p}{f(\bool)(u)} = f(\bool)(u).\]
  Finally, as discussed in \cref{sec:compute-universe}, transporting in the type family $A\mapsto A$ along the path $p\jdeq \ua(e)$ is equivalent to applying the equivalence $e$; thus we have
  \begin{equation}
    e(f(\bool)(u)) = f(\bool)(u).\label{eq:fpaut}
  \end{equation}
  %
  However, we can also prove that
  \begin{equation}
    \prd{x:\bool} \neg(e(x)=x).\label{eq:fpfaut}
  \end{equation}
  This follows from a case analysis on $x$: both cases are immediate from the definition of $e$ and the fact that $\bfalse\neq\btrue$ (\cref{rmk:true-neq-false}).
  Thus, applying~\eqref{eq:fpfaut} to $f(\bool)(u)$ and~\eqref{eq:fpaut}, we obtain an element of $\emptyt$.
\end{proof}

\begin{rmk}
  \index{choice operator}%
  \indexsee{operator!choice}{choice operator}%
  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 \emph{natural}, and under the univalence axiom, all functions acting on types must be natural with respect to equivalences.
\end{rmk}

\begin{rmk}
  It is, however, still the case that $\neg\neg\neg A \to \neg A$ for any $A$; see \cref{ex:neg-ldn}.
\end{rmk}

\begin{cor}\label{thm:not-lem}
  \index{excluded middle}%
  It is not the case that for all $A:\UU$ we have $A+(\neg A)$.
\end{cor}
\begin{proof}
  Suppose we had $g:\prd{A:\UU} (A+(\neg A))$.
  We will show that then $\prd{A:\UU} (\neg\neg A \to A)$, so that we can apply \cref{thm:not-dneg}.
  Thus, suppose $A:\UU$ 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)\jdeq \inl(a)$ for some $a:A$, or $g(A)\jdeq \inr(w)$ for some $w:\neg A$.
  In the first case, we have $a:A$, while in the second case we have $u(w):\emptyt$ and so we can obtain anything we wish (such as $A$).
  Thus, in both cases we have an element of $A$, as desired.
\end{proof}

Thus, if we want to assume the univalence axiom (which, of course, we do) and still leave ourselves the option of classical\index{mathematics!classical} reasoning (which is also desirable), we cannot use the unmodified propositions-as-types principle to interpret \emph{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 \cref{subsec:when-trunc} we will return to the question of which logic to use when.
\index{anger|)}%
\index{proposition!as types|)}%
\index{logic!constructive vs classical|)}%

\section{Mere propositions}
\label{subsec:hprops}

\index{logic!of mere propositions|(}%
\index{mere proposition|(defstyle}%
\indexsee{proposition!mere}{mere proposition}%
We have seen that the propositions-as-types logic has both good and bad properties.
Both have a common cause: when types are viewed as propositions, they can contain more information than mere truth or falsity, and all ``logical'' constructions on them must respect this additional information.
This suggests that we could obtain a more conventional logic by restricting attention to types that do \emph{not} contain any more information than a truth value, and only regarding these as logical propositions.

Such a type $A$ will be ``true'' if it is inhabited, and ``false'' if its inhabitation yields a contradiction (i.e.\ if $\neg A \jdeq (A\to\emptyt)$ is inhabited).
\index{inhabited type}%
What we want to avoid, in order to obtain a more traditional sort of logic, is treating as logical propositions those types for which giving an element of them gives more information than simply knowing that the type is inhabited.
For instance, if we are given an element of \bool, then we receive more information than the mere fact that \bool contains some element.
Indeed, we receive exactly \emph{one bit}
\index{bit}%
more information: we know \emph{which} element of \bool we were given.
By contrast, if we are given an element of \unit, then we receive no more information than the mere fact that \unit contains an element, since any two elements of \unit are equal to each other.
This suggests the following definition.

\begin{defn}\label{defn:isprop}
  A type $P$ is a \define{mere proposition}
  if for all $x,y:P$ we have $x=y$.
\end{defn}

Note that since we are still doing mathematics \emph{in} type theory, this is a definition \emph{in} type theory, which means it is a type --- or, rather, a type family.
Specifically, for any $P:\type$, the type $\isprop(P)$ is defined to be
\[ \isprop(P) \defeq \prd{x,y:P} (x=y). \]
Thus, to assert that ``$P$ is a mere proposition'' means to exhibit an inhabitant of $\isprop(P)$, which is a dependent function connecting any two elements of $P$ by a path.
The continuity/naturality of this function implies that not only are any two elements of $P$ equal, but $P$ contains no higher homotopy either.

\begin{lem}\label{thm:inhabprop-eqvunit}
  If $P$ is a mere proposition and $x_0:P$, then $\eqv P \unit$.
\end{lem}
\begin{proof}
  Define $f:P\to\unit$ by $f(x)\defeq \ttt$, and $g:\unit\to P$ by $g(u)\defeq x_0$.
  The claim follows from the next lemma, and the observation that \unit is a mere proposition by \cref{thm:path-unit}.
\end{proof}

\begin{lem}\label{lem:equiv-iff-hprop}
  If $P$ and $Q$ are mere propositions such that $P\to Q$ and $Q\to P$, then $\eqv P Q$.
\end{lem}
\begin{proof}
  Suppose given $f:P\to Q$ and $g:Q\to P$.
  Then for any $x:P$, we have $g(f(x))=x$ since $P$ is a mere proposition.
  Similarly, for any $y:Q$ we have $f(g(y))=y$ since $Q$ is a mere proposition; thus $f$ and $g$ are quasi-inverses.
\end{proof}

That is, as promised in \cref{sec:pat}, if two mere propositions are logically equivalent, then they are equivalent.

In homotopy theory, a space that is homotopy equivalent to \unit is said to be \emph{contractible}.
Thus, any mere proposition which is inhabited is contractible (see also \cref{sec:contractibility}).
On the other hand, the uninhabited type \emptyt is also (vacuously) a mere proposition.
In classical\index{mathematics!classical} mathematics, at least, these are the only two possibilities.

Mere propositions are also called \emph{subterminal objects} (if thinking categorically), \emph{subsingletons} (if thinking set-theoretically), or \emph{h-propositions}.
\indexsee{object!subterminal}{mere proposition}%
\indexsee{subterminal object}{mere proposition}%
\indexsee{subsingleton}{mere proposition}%
\indexsee{h-proposition}{mere proposition}
The discussion in \cref{sec:basics-sets} suggests we should also call them \emph{$(-1)$-types}; we will return to this in \cref{cha:hlevels}.
The adjective ``mere'' emphasizes that although any type may be regarded as a proposition (which we prove by giving an inhabitant of it), a type that is a mere proposition cannot usefully be regarded as any \emph{more} than a proposition: there is no additional information contained in a witness of its truth.

Note that a type $A$ is a set if and only if for all $x,y:A$, the identity type $\id[A]xy$ is a mere proposition.
On the other hand, by copying and simplifying the proof of \cref{thm:isset-is1type}, we have:

\begin{lem}\label{thm:prop-set}
  Every mere proposition is a set.
\end{lem}
\begin{proof}
  Suppose $f:\isprop(A)$; thus for all $x,y:A$ we have $f(x,y):x=y$.  Fix $x:A$
  and define $g(y)\defeq f(x,y)$.   Then for any $y,z:A$ and $p:y=z$ we have $\apd
  g p : \trans{p}{g(y)}={g(z)}$.  Hence by \cref{cor:transport-path-prepost}, we have
  $g(y)\ct p = g(z)$, which is to say that $p=\opp{g(y)}\ct g(z)$.  Thus, for
  any $p,q:x=y$, we have $p = \opp{g(x)}\ct g(y) = q$.
\end{proof}

In particular, this implies:

\begin{lem}\label{thm:isprop-isprop}\label{thm:isprop-isset}
  For any type $A$, the types $\isprop(A)$ and $\isset(A)$ are mere propositions.
\end{lem}
\begin{proof}
  Suppose $f,g:\isprop(A)$.  By function extensionality, to show $f=g$ it
  suffices to show $f(x,y)=g(x,y)$ for any $x,y:A$.  But $f(x,y)$ and $g(x,y)$
  are both paths in $A$, and hence are equal because, by either $f$ or $g$, we
  have that $A$ is a mere proposition, and hence by \cref{thm:prop-set} is a
  set.  Similarly, suppose $f,g:\isset(A)$, which is to say that for all
  $a,b:A$ and $p,q:a=b$, we have $f(a,b,p,q):p=q$ and $g(a,b,p,q):p=q$.  But by then since $A$ is a set (by
  either $f$ or $g$), and hence a 1-type, it follows that $f(a,b,p,q)=g(a,b,p,q)$; hence $f=g$ by
  function extensionality.
\end{proof}

We have seen one other example so far: condition~\ref{item:be3} in \cref{sec:basics-equivalences} asserts that for any function $f$, the type $\isequiv (f)$ should be a mere proposition.

\index{logic!of mere propositions|)}%
\index{mere proposition|)}%

\section{Classical vs.\ intuitionistic logic}
\label{sec:intuitionism}

\index{logic!constructive vs classical|(}%
\index{denial|(}%
With the notion of mere proposition in hand, we can now give the proper formulation of the \define{law of excluded middle}
\indexdef{excluded middle}%
\indexsee{axiom!excluded middle}{excluded middle}%
\indexsee{law!of excluded middle}{excluded middle}%
in homotopy type theory:
\begin{equation}
  \label{eq:lem}
  \LEM{}\;\defeq\;
  \prd{A:\UU} \Big(\isprop(A) \to (A + \neg A)\Big).
\end{equation}
Similarly, the \define{law of double negation}
\indexdef{double negation, law of}%
\indexdef{axiom!double negation}%
\indexdef{law!of double negation}%
is
\begin{equation}
  \label{eq:ldn}
  % \mathsf{DN}\;\defeq\;
  \prd{A:\UU} \Big(\isprop(A) \to (\neg\neg A \to A)\Big).
\end{equation}
The two are also easily seen to be equivalent to each other---see \cref{ex:lem-ldn}---so from now on we will generally speak only of \LEM{}.

This formulation of \LEM{} avoids the ``paradoxes'' of \cref{thm:not-dneg,thm:not-lem}, since \bool is not a mere proposition.
In order to distinguish it from the more general propositions-as-types formulation, we rename the latter:
\symlabel{lem-infty}
\begin{equation*}
  \LEM\infty \defeq \prd{A:\UU} (A + \neg A).
\end{equation*}
For emphasis, the proper version~\eqref{eq:lem}
may be denoted $\LEM{-1}$;
see also \cref{ex:lemnm}.
Although $\LEM{}$
is not a consequence of the basic type theory described in \cref{cha:typetheory}, it may be consistently assumed as an axiom (unlike its $\infty$-counterpart).
For instance, we will assume it in \cref{sec:wellorderings}.

However, it can be surprising how far we can get without using \LEM{}.
Quite often, a simple reformulation of a definition or theorem enables us to avoid invoking excluded middle.
While this takes a little getting used to sometimes, it is often worth the hassle, resulting in more elegant and more general proofs.
We discussed some of the benefits of this in the introduction.

For instance, in classical\index{mathematics!classical} mathematics, double negations are frequently used unnecessarily.
A very simple example is the common assumption that a set $A$ is ``nonempty'', which literally means it is \emph{not} the case that $A$ contains \emph{no} elements.
Almost always what is really meant is the positive assertion that $A$ \emph{does} contain at least one element, and by removing the double negation we make the statement less dependent on \LEM{}.
Recall that we say that a type $A$ is \emph{inhabited}
\index{inhabited type}%
when we assert $A$ itself as a proposition (i.e.\ we construct an element of $A$, usually unnamed).
Thus, often when translating a classical proof into constructive logic, we replace the word ``nonempty'' by ``inhabited'' (although sometimes we must replace it instead by ``merely inhabited''; see \cref{subsec:prop-trunc}).

Similarly, it is not uncommon in classical mathematics to find unnecessary proofs by contradiction.
\index{proof!by contradiction}%
Of course, the classical form of proof by contradiction proceeds by way of the law of double negation: we assume $\neg A$ and derive a contradiction, thereby deducing $\neg \neg A$, and thus by double negation we obtain $A$.
However, often the derivation of a contradiction from $\neg A$ can be rephrased slightly so as to yield a direct proof of $A$, avoiding the need for \LEM{}.

It is also important to note that if the goal is to prove a \emph{negation}\index{negation}, then ``proof by contradiction'' does not involve \LEM{}.
In fact, since $\neg A$ is by definition the type $A\to\emptyt$, by definition to prove $\neg A$ is to prove a contradiction (\emptyt) under the assumption of $A$.
Similarly, the law of double negation does hold for negated propositions: $\neg\neg\neg A \to \neg A$.
With practice, one learns to distinguish more carefully between negated and non-negated propositions and to notice when \LEM{} is being used and when it is not.

Thus, contrary to how it may appear on the surface, doing mathematics ``constructively'' does not usually involve giving up important theorems, but rather finding the best way to state the definitions so as to make the important theorems constructively provable.
That is, we may freely use the \LEM{} when first investigating a subject, but once that subject is better understood, we can hope to refine its definitions and proofs so as to avoid that axiom.
% For instance, the theory of ordinal numbers, which classically makes heavy use of \LEM{}, works quite well constructively once we choose the correct definition of ``ordinal''; see \cref{sec:ordinals}.
This sort of observation is even more pronounced in \emph{homotopy} type theory, where the powerful tools of univalence and higher inductive types allow us to constructively attack many problems that traditionally would require classical\index{mathematics!classical} reasoning.
We will see several examples of this in \cref{part:mathematics}.
% For instance, none of the ``synthetic'' homotopy theory we will develop in \cref{cha:homotopy} requires \LEM{} --- despite the fact that classical homotopy theory (formulated using topological spaces or simplicial sets) makes heavy use of them (as well as the axiom of choice).

It is also worth mentioning that even in constructive mathematics, the law of excluded middle can hold for \emph{some} propositions.
The name traditionally given to such propositions is \emph{decidable}.

\begin{defn}\label{defn:decidable-equality}
  \mbox{}
  \begin{enumerate}
  \item A type $A$ is called \define{decidable}
    \indexdef{decidable!type}%
    \indexdef{type!decidable}%
    if $A+\neg A$.
  \item Similarly, a type family $B:A\to \type$ is \define{decidable}
    \indexdef{decidable!type family}%
    \indexdef{type!family of!decidable}%
    if \narrowequation{\prd{a:A} (B(a)+\neg B(a)).} \label{item:decidable-equality2}
  \item In particular, $A$ has \define{decidable equality}
    \indexdef{decidable!equality}%
    \indexsee{equality!decidable}{decidable equality}%
    if \narrowequation{\prd{a,b:A} ((a=b) + \neg(a=b)).}
  \end{enumerate}
\end{defn}

Thus, $\LEM{}$ is exactly the statement that all mere propositions are decidable, and hence so are all families of mere propositions.
In particular, $\LEM{}$ implies that all sets (in the sense of \cref{sec:basics-sets}) have decidable equality.
Having decidable equality in this sense is very strong; see \cref{thm:hedberg}.

\index{denial|)}%
\index{logic!constructive vs classical|)}%

\section{Subsets and propositional resizing}
\label{subsec:prop-subsets}

\index{mere proposition|(}%

As another example of the usefulness of mere propositions, we discuss subsets (and more generally subtypes).
Suppose $P:A\to\type$ is a type family, with each type $P(x)$ regarded as a proposition.
Then $P$ itself is a \emph{predicate} on $A$, or a \emph{property} of elements of $A$.

In set theory, whenever we have a predicate $P$ on a set $A$, we may form the subset $\setof{x\in A | P(x)}$.
As mentioned briefly in \cref{sec:pat}, the obvious analogue in type theory is the $\Sigma$-type $\sm{x:A} P(x)$.
An inhabitant of $\sm{x:A} P(x)$ is, of course, a pair $(x,p)$ where $x:A$ and $p$ is a proof of $P(x)$.
However, for general $P$, an element $a:A$ might give rise to more than one distinct element of $\sm{x:A} P(x)$, if the proposition $P(a)$ has more than one distinct proof.
This is counter to the usual intuition of a subset.
But if $P$ is a \emph{mere} proposition, then this cannot happen.

\begin{lem}\label{thm:path-subset}
  Suppose $P:A\to\type$ is a type family such that $P(x)$ is a mere proposition for all $x:A$.
  If $u,v:\sm{x:A} P(x)$ are such that $\proj1(u) = \proj1(v)$, then $u=v$.
\end{lem}
\begin{proof}
  Suppose $p:\proj1(u) = \proj1(v)$.
  By \cref{thm:path-sigma}, to show $u=v$ it suffices to show $\trans{p}{\proj2(u)} = \proj2(v)$.
  But $\trans{p}{\proj2(u)}$ and $\proj2(v)$ are both elements of $P(\proj1(v))$, which is a mere proposition; hence they are equal.
\end{proof}

For instance, recall that in \cref{sec:basics-equivalences} we defined
\[(\eqv A B) \;\defeq\; \sm{f:A\to B} \isequiv (f),\]
where each type $\isequiv (f)$ was supposed to be a mere proposition.
It follows that if two equivalences have equal underlying functions, then they are equal as equivalences.

\label{defn:setof}%
Henceforth, if $P:A\to \type$ is a family of mere propositions (i.e.\ each $P(x)$ is a mere proposition), we may write
%
\begin{equation}
  \label{eq:subset}
  \setof{x:A | P(x)}
\end{equation}
%
as an alternative notation for $\sm{x:A} P(x)$.
(There is no technical reason not to use this notation for arbitrary $P$ as well, but such usage could be confusing due to unintended connotations.)
If $A$ is a set, we call \eqref{eq:subset} a \define{subset}
\indexdef{subset}%
\indexdef{type!subset}%
of $A$; for general $A$ we might call it a \define{subtype}.
\indexdef{subtype}%
We may also refer to $P$ itself as a \emph{subset} or \emph{subtype} of $A$; this is actually more correct, since the type~\eqref{eq:subset} in isolation doesn't remember its relationship to $A$.

\symlabel{membership}
Given such a $P$ and $a:A$, we may write $a\in P$ or $a\in \setof{x:A | P(x)}$ to refer to the mere proposition $P(a)$.
If it holds, we may say that $a$ is a \define{member} of $P$.
\symlabel{subset}
Similarly, if $\setof{x:A | Q(x)}$ is another subset of $A$, then we say that $P$ is \define{contained}
\indexdef{containment!of subsets}%
\indexdef{inclusion!of subsets}%
in $Q$, and write $P\subseteq Q$, if we have $\prd{x:A}(P(x)\rightarrow Q(x))$.

As further examples of subtypes, we may define the ``subuniverses'' of sets and of mere propositions in a universe \UU:
\symlabel{setU}\symlabel{propU}
\begin{align*}
  \setU &\defeq \setof{A:\UU | \isset(A) },\\
  \propU &\defeq \setof{A:\UU | \isprop(A) }.
\end{align*}
An element of $\setU$ is a type $A:\UU$ together with evidence $s:\isset(A)$, and similarly for $\propU$.
\cref{thm:path-subset} implies that $\id[\setU]{(A,s)}{(B,t)}$ is equivalent to $\id[\UU]AB$ (and hence to $\eqv AB$).
Thus, we will frequently abuse notation and write simply $A:\setU$ instead of $(A,s):\setU$.
We may also drop the subscript \UU if there is no need to specify the universe in question.

Recall that for any two universes $\UU_i$ and $\UU_{i+1}$, if $A:\UU_i$ then also $A:\UU_{i+1}$.
Thus, for any $(A,s):\set_{\UU_i}$ we also have $(A,s):\set_{\UU_{i+1}}$, and similarly for $\prop_{\UU_i}$, giving natural maps
\begin{align}
  \set_{\UU_i} &\to \set_{\UU_{i+1}}\label{eq:set-up},\\
  \prop_{\UU_i} &\to \prop_{\UU_{i+1}}.\label{eq:prop-up}
\end{align}
The map~\eqref{eq:set-up} cannot be an equivalence, since then we could reproduce the paradoxes\index{paradox} of self-reference that are familiar from Cantorian set theory.
However, although~\eqref{eq:prop-up} is not automatically an equivalence in the type theory we have presented so far, it is consistent to suppose that it is.
That is, we may consider adding to type theory the following axiom.

\begin{axiom}[Propositional resizing]
  \indexsee{axiom!propositional resizing}{propositional resizing}%
  \indexdef{propositional!resizing}%
  \indexsee{resizing!propositional}{propositional resizing}%
  The map $\prop_{\UU_i} \to \prop_{\UU_{i+1}}$ is an equivalence.
\end{axiom}

We refer to this axiom as \define{propositional resizing},
since it means that any mere proposition in the universe $\UU_{i+1}$ can be ``resized'' to an equivalent one in the smaller universe $\UU_i$.
It follows automatically if $\UU_{i+1}$ satisfies \LEM{} (see \cref{ex:lem-impred}).
We will not assume this axiom in general, although in some places we will use it as an explicit hypothesis.
It is a form of \emph{impredicativity} for mere propositions, and by avoiding its use, the type theory is said to remain \emph{predicative}.
\indexsee{impredicativity!for mere propositions}{propositional resizing}%
\indexdef{mathematics!predicative}%

In practice, what we want most frequently is a slightly different statement: that a universe \UU under consideration contains a type which ``classifies all mere propositions''.
In other words, we want a type $\Omega:\UU$ together with an $\Omega$-indexed family of mere propositions, which contains every mere proposition up to equivalence.
This statement follows from propositional resizing as stated above if $\UU$ is not the smallest universe $\UU_0$, since then we can define $\Omega\defeq \prop_{\UU_0}$.

One use for impredicativity is to define power sets.
It is natural to define the \define{power set}\indexdef{power set} of a set $A$ to be $A\to\propU$; but in the absence of impredicativity, this definition depends
(even up to equivalence) on the choice of the universe \UU.
But with propositional resizing, we can define the power set to be
\symlabel{powerset}%
\[ \power A \defeq (A\to\Omega),\]
which is then independent of $\UU$.
See also \cref{subsec:piw}.


\section{The logic of mere propositions}
\label{subsec:logic-hprop}

\index{logic!of mere propositions|(}%
We mentioned in \cref{sec:types-vs-sets} that in contrast to type theory, which has only one basic notion (types), set-theoretic foundations have two basic notions: sets and propositions.
Thus, a classical\index{mathematics!classical} mathematician is accustomed to manipulating these two kinds of objects separately.

It is possible to recover a similar dichotomy in type theory, with the role of the set-theoretic propositions being played by the types (and type families) that are \emph{mere} propositions.
In many cases, the logical connectives and quantifiers can be represented in this logic by simply restricting the corresponding type-former to the mere propositions.
Of course, this requires knowing that the type-former in question preserves mere propositions.

\begin{eg}
  If $A$ and $B$ are mere propositions, so is $A\times B$.
  This is easy to show using the characterization of paths in products, just like \cref{thm:isset-prod} but simpler.
  Thus, the connective ``and'' preserves mere propositions.
\end{eg}

\begin{eg}\label{thm:isprop-forall}
  If $A$ is any type and $B:A\to \type$ is such that for all $x:A$, the type $B(x)$ is a mere proposition, then $\prd{x:A} B(x)$ is a mere proposition.
  The proof is just like \cref{thm:isset-forall} but simpler: given $f,g:\prd{x:A} B(x)$, for any $x:A$ we have $f(x)=g(x)$ since $B(x)$ is a mere proposition.
  But then by function extensionality, we have $f=g$.

  In particular, if $B$ is a mere proposition, then so is $A\to B$ regardless of what $A$ is.
  In even more particular, since \emptyt is a mere proposition, so is $\neg A \jdeq (A\to\emptyt)$.
  \index{quantifier!universal}%
  Thus, the connectives ``implies'' and ``not'' preserve mere propositions, as does the quantifier ``for all''.
\end{eg}

On the other hand, some type formers do not preserve mere propositions.
Even if $A$ and $B$ are mere propositions, $A+B$ will not in general be.
For instance, \unit is a mere proposition, but $\bool=\unit+\unit$ is not.
Logically speaking, $A+B$ is a ``purely constructive'' sort of ``or'': a witness of it contains the additional information of \emph{which} disjunct is true.
Sometimes this is very useful, but if we want a more classical sort of ``or'' that preserves mere propositions, we need a way to ``truncate'' this type into a mere proposition by forgetting this additional information.

\index{quantifier!existential}%
The same issue arises with the $\Sigma$-type $\sm{x:A} P(x)$.
This is a purely constructive interpretation of ``there exists an $x:A$ such that $P(x)$'' which remembers the witness $x$, and hence is not generally a mere proposition even if each type $P(x)$ is.
(Recall that we observed in \cref{subsec:prop-subsets} that $\sm{x:A} P(x)$ can also be regarded as ``the subset of those $x:A$ such that $P(x)$''.)


\section{Propositional truncation}
\label{subsec:prop-trunc}

\index{truncation!propositional|(defstyle}%
\indexsee{type!squash}{truncation, propositional}%
\indexsee{squash type}{truncation, propositional}%
\indexsee{bracket type}{truncation, propositional}%
\indexsee{type!bracket}{truncation, propositional}%
The \emph{propositional truncation}, also called the \emph{$(-1)$-truncation}, \emph{bracket type}, or \emph{squash type}, is an additional type former which ``squashes'' or ``truncates'' a type down to a mere proposition, forgetting all information contained in inhabitants of that type other than their existence.

More precisely, for any type $A$, there is a type $\brck{A}$.
It has two constructors:
\begin{itemize}
\item For any $a:A$ we have $\bproj a : \brck A$.
\item For any $x,y:\brck A$, we have $x=y$.
\end{itemize}
The first constructor means that if $A$ is inhabited, so is $\brck A$.
The second ensures that $\brck A$ is a mere proposition; usually we leave the witness of this fact nameless.

\index{recursion principle!for truncation}%
The recursion principle of $\brck A$ says that:
\begin{itemize}
\item If $B$ is a mere proposition and we have $f:A\to B$, then there is an induced $g:\brck A \to B$ such that $g(\bproj a) \jdeq f(a)$ for all $a:A$.
\end{itemize}
In other words, any mere proposition which follows from (the inhabitedness of) $A$ already follows from $\brck A$.
Thus, $\brck A$, as a mere proposition, contains no more information than the inhabitedness of $A$.
(There is also an induction principle for $\brck A$, but it is not especially useful; see \cref{ex:prop-trunc-ind}.)

In \cref{ex:lem-brck,ex:impred-brck,sec:hittruncations} we will describe some ways to construct $\brck{A}$ in terms of more general things.
For now, we simply assume it as an additional rule alongside those of \cref{cha:typetheory}.

With the propositional truncation, we can extend the ``logic of mere propositions'' to cover disjunction and the existential quantifier.
Specifically, $\brck{A+B}$ is a mere propositional version of ``$A$ or $B$'', which does not ``remember'' the information of which disjunct is true.

The recursion principle of truncation implies that we can still do a case analysis on $\brck{A+B}$ \emph{when attempting to prove a mere proposition}.
That is, suppose we have an assumption $u:\brck{A+B}$ and we are trying to prove a mere proposition $Q$.
In other words, we are trying to define an element of $\brck{A+B} \to Q$.
Since $Q$ is a mere proposition, by the recursion principle for propositional truncation, it suffices to construct a function $A+B\to Q$.
But now we can use case analysis on $A+B$.

Similarly, for a type family $P:A\to\type$, we can consider $\brck{\sm{x:A} P(x)}$, which is a mere propositional version of ``there exists an $x:A$ such that $P(x)$''.
As for disjunction, by combining the induction principles of truncation and $\Sigma$-types, if we have an assumption of type $\brck{\sm{x:A} P(x)}$, we may introduce new assumptions $x:A$ and $y:P(x)$ \emph{when attempting to prove a mere proposition}.
In other words, if we know that there exists some $x:A$ such that $P(x)$, but we don't have a particular such $x$ in hand, then we are free to make use of such an $x$ as long as we aren't trying to construct anything which might depend on the particular value of $x$.
Requiring the codomain to be a mere proposition expresses this independence of the result on the witness, since all possible inhabitants of such a type must be equal.

For the purposes of set-level mathematics in \cref{cha:real-numbers,cha:set-math},
where we deal mostly with sets and mere propositions, it is convenient to use the
traditional logical notations to refer only to ``propositionally truncated logic''.

\begin{defn} \label{defn:logical-notation}
  We define \define{traditional logical notation}
  \indexdef{implication}%
  \indexdef{traditional logical notation}%
  \indexdef{logical notation, traditional}%
  \index{quantifier}%
  \indexsee{existential quantifier}{quantifier, existential}%
  \index{quantifier!existential}%
  \indexsee{universal!quantifier}{quantifier, universal}%
  \index{quantifier!universal}%
  \indexdef{conjunction}%
  \indexdef{disjunction}%
  \indexdef{true}%
  \indexdef{false}%
  using truncation as follows, where $P$ and $Q$ denote mere propositions (or families thereof):
  {\allowdisplaybreaks
  \begin{align*}
    \top            &\ \defeq \ \unit \\
    \bot            &\ \defeq \ \emptyt \\
    P \land Q       &\ \defeq \ P \times Q \\
    P \Rightarrow Q &\ \defeq \ P \to Q \\
    P \Leftrightarrow Q &\ \defeq \ P = Q \\
    \neg P          &\ \defeq \ P \to \emptyt \\
    P \lor Q        &\ \defeq \ \brck{P + Q} \\
    \fall{x : A} P(x) &\ \defeq \ \prd{x : A} P(x) \\
    \exis{x : A} P(x) &\ \defeq \ \Brck{\sm{x : A} P(x)}
  \end{align*}}
\end{defn}

The notations $\land$ and $\lor$ are also used in homotopy theory for the smash product and the wedge of pointed spaces, which we will introduce in \cref{cha:hits}.
This technically creates a potential for conflict, but no confusion will generally arise.

Similarly, when discussing subsets as in \cref{subsec:prop-subsets}, we may use the traditional notation for intersections, unions, and complements:
\indexdef{intersection!of subsets}%
\symlabel{intersection}%
\indexdef{union!of subsets}%
\symlabel{union}%
\indexdef{complement, of a subset}%
\symlabel{complement}%
\begin{align*}
  \setof{x:A | P(x)} \cap \setof{x:A | Q(x)}
  &\defeq \setof{x:A | P(x) \land Q(x)},\\
  \setof{x:A | P(x)} \cup \setof{x:A | Q(x)}
  &\defeq \setof{x:A | P(x) \lor Q(x)},\\
  A \setminus \setof{x:A | P(x)}
  &\defeq \setof{x:A | \neg P(x)}.
\end{align*}
Of course, in the absence of \LEM{}, the latter are not ``complements'' in the usual sense: we may not have $B \cup (A\setminus B) = A$ for every subset $B$ of $A$.

\index{truncation!propositional|)}%
\index{mere proposition|)}%
\index{logic!of mere propositions|)}%


\section{The axiom of choice}
\label{sec:axiom-choice}

\index{axiom!of choice|(defstyle}%
\index{denial|(}%
We can now properly formulate the axiom of choice in homotopy type theory.
Assume a type $X$ and type families
%
\begin{equation*}
  A:X\to\type
  \qquad\text{and}\qquad
  P:\prd{x:X} A(x)\to\type,
\end{equation*}
%
and moreover that
\begin{itemize}
\item $X$ is a set,
\item $A(x)$ is a set for all $x:X$, and
\item $P(x,a)$ is a mere proposition for all $x:X$ and $a:A(x)$.
\end{itemize}
The \define{axiom of choice}
$\choice{}$ asserts that under these assumptions,
\begin{equation}\label{eq:ac}
  \Parens{\prd{x:X} \Brck{\sm{a:A(x)} P(x,a)}}
  \to
  \Brck{\sm{g:\prd{x:X} A(x)} \prd{x:X} P(x,g(x))}.
\end{equation}
Of course, this is a direct translation of~\eqref{eq:english-ac} where we read ``there exists $x:A$ such that $B(x)$'' as $\brck{\sm{x:A}B(x)}$, so we could have written the statement in the familiar logical notation as
\begin{narrowmultline*}
  \textstyle
  \Big(\fall{x:X}\exis{a:A(x)} P(x,a)\Big)
  \Rightarrow \narrowbreak
  \Big(\exis{g : \prd{x:X} A(x)} \fall{x : X} P(x,g(x))\Big).
\end{narrowmultline*}
%
In particular, note that the propositional truncation appears twice.
The truncation in the domain means we assume that for every $x$ there exists some $a:A(x)$ such that $P(x,a)$, but that these values are not chosen or specified in any known way.
The truncation in the codomain means we conclude that there exists some function $g$, but this function is not determined or specified in any known way.

In fact, because of \cref{thm:ttac}, this axiom can also be expressed in a simpler form.

\begin{lem}\label{thm:ac-epis-split}
  The axiom of choice~\eqref{eq:ac} is equivalent to the statement that for any set $X$ and any $Y:X\to\type$ such that each $Y(x)$ is a set, we have
  \begin{equation}
    \Parens{\prd{x:X} \Brck{Y(x)}}
    \to
    \Brck{\prd{x:X} Y(x)}.\label{eq:epis-split}
  \end{equation}
\end{lem}

This corresponds to a well-known equivalent form of the classical\index{mathematics!classical} axiom of choice, namely ``the cartesian product of a family of nonempty sets is nonempty''.

\begin{proof}
  By \cref{thm:ttac}, the codomain of~\eqref{eq:ac} is equivalent to
  \[\Brck{\prd{x:X} \sm{a:A(x)} P(x,a)}.\]
  Thus,~\eqref{eq:ac} is equivalent to the instance of~\eqref{eq:epis-split} where \narrowequation{Y(x) \defeq \sm{a:A(x)} P(x,a).}
  (This is a set by \cref{thm:isset-prod,thm:prop-set}.)
  Conversely,~\eqref{eq:epis-split} is equivalent to the instance of~\eqref{eq:ac} where $A(x)\defeq Y(x)$ and $P(x,a)\defeq\unit$.
  Thus, the two are logically equivalent.
  Since both are mere propositions, by \cref{lem:equiv-iff-hprop} they are equivalent types.
\end{proof}

As with \LEM{}, the equivalent forms~\eqref{eq:ac} and~\eqref{eq:epis-split} are not a consequence of our basic type theory, but they may consistently be assumed as axioms.

\begin{rmk}
  It is easy to show that the right side of~\eqref{eq:epis-split} always implies the left.
  Since both are mere propositions, by \cref{lem:equiv-iff-hprop} the axiom of choice is also equivalent to asking for an equivalence
  \[ \eqv{\Parens{\prd{x:X} \Brck{Y(x)}}}{\Brck{\prd{x:X} Y(x)}} \]
  This illustrates a common pitfall: although dependent function types preserve mere propositions (\cref{thm:isprop-forall}), they do not commute with truncation: $\brck{\prd{x:A} P(x)}$ is not generally equivalent to $\prd{x:A} \brck{P(x)}$.
  The axiom of choice, if we assume it, says that this is true \emph{for sets}; as we will see below, it fails in general.
\end{rmk}

The restriction in the axiom of choice to types that are sets can be relaxed to a certain extent.
For instance, we may allow $A$ and $P$ in~\eqref{eq:ac}, or $Y$ in~\eqref{eq:epis-split}, to be arbitrary type families; this results in a seemingly stronger statement that is equally consistent.
We may also replace the propositional truncation by the more general $n$-truncations to be considered in \cref{cha:hlevels}, obtaining a spectrum of axioms $\choice n$ interpolating between~\eqref{eq:ac}, which we call simply \choice{} (or $\choice{-1}$ for emphasis), and \cref{thm:ttac}, which we shall call $\choice\infty$.
See also \cref{ex:acnm,ex:acconn}.
However, observe that we cannot relax the requirement that $X$ be a set.

\begin{lem}\label{thm:no-higher-ac}
  There exists a type $X$ and a family $Y:X\to \type$ such that each $Y(x)$ is a set, but such that~\eqref{eq:epis-split} is false.
\end{lem}
\begin{proof}
  Define $X\defeq \sm{A:\type} \brck{\bool = A}$, and let $x_0 \defeq (\bool, \bproj{\refl{\bool}}) : X$.
  Then by the identification of paths in $\Sigma$-types, the fact that $\brck{A=\bool}$ is a mere proposition, and univalence, for any $(A,p),(B,q):X$ we have $\eqv{(\id[X]{(A,p)}{(B,q)})}{(\eqv AB)}$.
  In particular, $\eqv{(\id[X]{x_0}{x_0})}{(\eqv \bool\bool)}$, so as in \cref{thm:type-is-not-a-set}, $X$ is not a set.

  On the other hand, if $(A,p):X$, then $A$ is a set; this follows by induction on truncation for $p:\brck{\bool=A}$ and the fact that $\bool$ is a set.
  Since $\eqv A B$ is a set whenever $A$ and $B$ are, it follows that $\id[X]{x_1}{x_2}$ is a set for any $x_1,x_2:X$, i.e.\ $X$ is a 1-type.
  In particular, if we define $Y:X\to\UU$ by $Y(x) \defeq (x_0=x)$, then each $Y(x)$ is a set.

  Now by definition, for any $(A,p):X$ we have $\brck{\bool=A}$, and hence $\brck{x_0 = (A,p)}$.
  Thus, we have $\prd{x:X} \brck{Y(x)}$.
  If~\eqref{eq:epis-split} held for this $X$ and $Y$, then we would also have $\brck{\prd{x:X} Y(x)}$.
  Since we are trying to derive a contradiction ($\emptyt$), which is a mere proposition, we may assume $\prd{x:X} Y(x)$, i.e.\ that $\prd{x:X} (x_0=x)$.
  But this implies $X$ is a mere proposition, and hence a set, which is a contradiction.
\end{proof}

\index{denial|)}%
\index{axiom!of choice|)}%

\section{The principle of unique choice}
\label{sec:unique-choice}

\index{unique!choice|(defstyle}%
\indexsee{axiom!of choice!unique}{unique choice}%

The following observation is trivial, but very useful.

\begin{lem}\label{thm:prop-equiv-trunc}
  If $P$ is a mere proposition, then $\eqv P {\brck P}$.
\end{lem}
\begin{proof}
  Of course, we have $P\to \brck{P}$ by definition.
  And since $P$ is a mere proposition, the universal property of $\brck P$ applied to $\idfunc[P] :P\to P$ yields $\brck P \to P$.
  These functions are quasi-inverses by \cref{lem:equiv-iff-hprop}.
\end{proof}

Among its important consequences is the following.

\begin{cor}[The principle of unique choice]\label{cor:UC}
  Suppose a type family $P:A\to \type$ such that
  \begin{enumerate}
  \item For each $x$, the type $P(x)$ is a mere proposition, and
  \item For each $x$ we have $\brck {P(x)}$.
  \end{enumerate}
  Then we have $\prd{x:A} P(x)$.
\end{cor}
\begin{proof}
  Immediate from the two assumptions and the previous lemma.
\end{proof}

The corollary also encapsulates a very useful technique of reasoning.
Namely, suppose we know that $\brck A$, and we want to use this to construct an element of some other type $B$.
We would like to use an element of $A$ in our construction of an element of $B$, but this is allowed only if $B$ is a mere proposition, so that we can apply the induction principle for the propositional truncation $\brck A$; the most we could hope to do in general is to show $\brck B$.
%
Instead, we can extend $B$ with additional data which characterizes \emph{uniquely} the object we wish to construct.
Specifically, we define a predicate $Q:B\to\type$ such that $\sm{x:B} Q(x)$ is a mere proposition.
Then from an element of $A$ we construct an element $b:B$ such that $Q(b)$, hence from $\brck A$ we can construct $\brck{\sm{x:B} Q(x)}$, and because $\brck{\sm{x:B} Q(x)}$ is equivalent to $\sm{x:B} Q(x)$ an element of $B$ may be projected from it.
An example can be found in \cref{ex:decidable-choice}.

A similar issue arises in set-theoretic mathematics, although it manifests slightly
differently. If we are trying to define a function $f: A \to B$, and depending on an
element $a : A$ we are able to prove mere existence of some $b : B$, we are not done yet
because we need to actually pinpoint an element of~$B$, not just prove its existence.
One option is of course to refine the argument to unique existence of $b : B$, as we did in type theory. But in set theory the problem can often be avoided more simply by an application of the axiom of choice, which picks the required elements for us.
In homotopy type theory, however, quite apart from any desire to avoid choice, the available forms of choice are simply less applicable, since they require that the domain of choice be a \emph{set}.
Thus, if $A$ is not a set (such as perhaps a universe $\UU$), there is no consistent form of choice that will allow us to simply pick an element of $B$ for each $a : A$ to use in defining $f(a)$.

\index{unique!choice|)}%


\section{When are propositions truncated?}
\label{subsec:when-trunc}

\index{logic!of mere propositions|(}%
\index{mere proposition|(}%
\index{logic!truncated}%

At first glance, it may seem that the truncated versions of $+$ and $\Sigma$ are actually closer to the informal mathematical meaning of ``or'' and ``there exists'' than the untruncated ones.
Certainly, they are closer to the \emph{precise} meaning of ``or'' and ``there exists'' in the first-order logic \index{first-order!logic} which underlies formal set theory, since the latter makes no attempt to remember any witnesses to the truth of propositions.
However, it may come as a surprise to realize that the practice of \emph{informal} mathematics is often more accurately described by the untruncated forms.

\index{prime number}%
For example, consider a statement like ``every prime number is either $2$ or odd''.
The working mathematician feels no compunction about using this fact not only to prove \emph{theorems} about prime numbers, but also to perform \emph{constructions} on prime numbers, perhaps doing one thing in the case of $2$ and another in the case of an odd prime.
The end result of the construction is not merely the truth of some statement, but a piece of data which may depend on the parity of the prime number.
Thus, from a type-theoretic perspective, such a construction is naturally phrased using the induction principle for the coproduct type ``$(p=2)+(p\text{ is odd})$'', not its propositional truncation.

Admittedly, this is not an ideal example, since ``$p=2$'' and ``$p$ is odd'' are mutually exclusive, so that $(p=2)+(p\text{ is odd})$ is in fact already a mere proposition and hence equivalent to its truncation (see \cref{ex:disjoint-or}).
More compelling examples come from the existential quantifier.
It is not uncommon to prove a theorem of the form ``there exists an $x$ such that \dots'' and then refer later on to ``the $x$ constructed in Theorem Y'' (note the definite article).
Moreover, when deriving further properties of this $x$, one may use phrases such as ``by the construction of $x$ in the proof of Theorem Y''.

A very common example is ``$A$ is isomorphic to $B$'', which strictly speaking means only that there exists \emph{some} isomorphism between $A$ and~$B$.
But almost invariably, when proving such a statement, one exhibits a specific isomorphism or proves that some previously known map is an isomorphism, and it often matters later on what particular isomorphism was given.

Set-theoretically trained mathematicians often feel a twinge of guilt at such ``abuses of language''.\index{abuse!of language}
We may attempt to apologize for them, expunge them from final drafts, or weasel out of them with vague words like ``canonical''.
The problem is exacerbated by the fact that in formalized set theory, there is technically no way to ``construct'' objects at all --- we can only prove that an object with certain properties exists.
Untruncated logic in type theory thus captures some common practices of informal mathematics that the set theoretic reconstruction obscures.
(This is similar to how the univalence axiom validates the common, but formally unjustified, practice of identifying isomorphic objects.)

On the other hand, sometimes truncated logic is essential.
We have seen this in the statements of \LEM{} and \choice{}; some other examples will appear later on in the book.
Thus, we are faced with the problem: when writing informal type theory, what should we mean by the words ``or'' and ``there exists'' (along with common synonyms such as ``there is'' and ``we have'')?

A universal consensus may not be possible.
Perhaps depending on the sort of mathematics being done, one convention or the other may be more useful --- or, perhaps, the choice of convention may be irrelevant.
In this case, a remark at the beginning of a mathematical paper may suffice to inform the reader of the linguistic conventions in use therein.
However, even after one overall convention is chosen, the other sort of logic will usually arise at least occasionally, so we need a way to refer to it.
More generally, one may consider replacing the propositional truncation with another operation on types that behaves similarly, such as the double negation operation $A\mapsto \neg\neg A$, or the $n$-truncations to be considered in \cref{cha:hlevels}.
As an experiment in exposition,  in what follows we will occasionally use \emph{adverbs}\index{adverb} to denote the application of such ``modalities'' as propositional truncation.

For instance, if untruncated logic is the default convention, we may use the adverb \define{merely}
\indexdef{merely}%
to denote propositional truncation.
Thus the phrase
\begin{center}
  ``there merely exists an $x:A$ such that $P(x)$''
\end{center}
indicates the type $\brck{\sm{x:A} P(x)}$.
Similarly, we will say that a type $A$ is \define{merely inhabited}
\indexdef{merely!inhabited}%
\indexdef{inhabited type!merely}%
to mean that its propositional truncation $\brck A$ is inhabited (i.e.\ that we have an unnamed element of it).
Note that this is a \emph{definition}\index{definition!of adverbs} of the adverb ``merely'' as it is to be used in our informal mathematical English, in the same way that we define nouns\index{noun} like ``group'' and ``ring'', and adjectives\index{adjective} like ``regular'' and ``normal'', to have precise mathematical meanings.
We are not claiming that the dictionary definition of ``merely'' refers to propositional truncation; the choice of word is meant only to remind the mathematician reader that a mere proposition contains ``merely'' the information of a truth value and nothing more.

On the other hand, if truncated logic is the current default convention, we may use an adverb such as \define{purely}
\indexdef{purely}%
or \define{constructively} to indicate its absence, so that
\begin{center}
``there purely exists an $x:A$ such that $P(x)$''
\end{center}
would denote the type $\sm{x:A} P(x)$.
We may also use ``purely'' or ``actually'' just to emphasize the absence of truncation, even when that is the default convention.

In this book we will continue using untruncated logic as the default convention, for a number of reasons.
\begin{enumerate}[label=(\arabic*)]
\item We want to encourage the newcomer to experiment with it, rather than sticking to truncated logic simply because it is more familiar.
\item Using truncated logic as the default in type theory suffers from the same sort of ``abuse of language''\index{abuse!of language} problems as set-theoretic foundations, which untruncated logic avoids.
  For instance, our definition of ``$\eqv A B$'' as the type of equivalences between $A$ and $B$, rather than its propositional truncation, means that to prove a theorem of the form ``$\eqv A B$'' is literally to construct a particular such equivalence.
  This specific equivalence can then be referred to later on.
\item We want to emphasize that the notion of ``mere proposition'' is not a fundamental part of type theory.
  As we will see in \cref{cha:hlevels}, mere propositions are just the second rung on an infinite ladder, and there are also many other modalities not lying on this ladder at all.
\item Many statements that classically are mere propositions are no longer so in homotopy type theory.
  Of course, foremost among these is equality.
\item On the other hand, one of the most interesting observations of homotopy type theory is that a surprising number of types are \emph{automatically} mere propositions, or can be slightly modified to become so, without the need for any truncation.
  (See \cref{thm:isprop-isprop,cha:equivalences,cha:hlevels,cha:category-theory,cha:set-math}.)
  Thus, although these types contain no data beyond a truth value, we can nevertheless use them to construct untruncated objects, since there is no need to use the induction principle of propositional truncation.
  This useful fact is more clumsy to express if propositional truncation is applied to all statements by default.
\item Finally, truncations are not very useful for most of the mathematics we will be doing in this book, so it is simpler to notate them explicitly when they occur.
\end{enumerate}

\index{mere proposition|)}%
\index{logic!of mere propositions|)}%

\section{Contractibility}
\label{sec:contractibility}

\index{type!contractible|(defstyle}%
\index{contractible!type|(defstyle}%

In \cref{thm:inhabprop-eqvunit} we observed that a mere proposition which is inhabited must be equivalent to $\unit$,
\index{type!unit}%
and it is not hard to see that the converse also holds.
A type with this property is called \emph{contractible}.
Another equivalent definition of contractibility, which is also sometimes convenient, is the following.

\begin{defn}\label{defn:contractible}
  A type $A$ is \define{contractible},
  or a \define{singleton},
  \indexdef{type!singleton}%
  \indexsee{singleton type}{type, singleton}%
  if there is $a:A$, called the \define{center of contraction},
  \indexdef{center!of contraction}%
  such that $a=x$ for all $x:A$.
  We denote the specified path $a=x$ by $\contr_x$.
\end{defn}

In other words, the type $\iscontr(A)$ is defined to be
\[ \iscontr(A) \defeq \sm{a:A} \prd{x:A}(a=x). \]
Note that under the usual propositions-as-types reading, we can pronounce $\iscontr(A)$ as ``$A$ contains exactly one element'', or more precisely ``$A$ contains an element, and every element of $A$ is equal to that element''.

\begin{rmk}
  We can also pronounce $\iscontr(A)$ more topologically as ``there is a point $a:A$ such that for all $x:A$ there exists a path from $a$ to $x$''.
  Note that to a classical ear, this sounds like a definition of \emph{connectedness} rather than contractibility.
  \index{continuity of functions in type theory@``continuity'' of functions in type theory}%
  \index{functoriality of functions in type theory@``functoriality'' of functions in type theory}%
  The point is that the meaning of ``there exists'' in this sentence is a continuous/natural one.

  A better way to express connectedness would be $\sm{a:A}\prd{x:A} \brck{a=x}$.
  This is indeed correct if $A$ is assumed to be pointed --- see the remark after \cref{thm:connected-pointed} --- but in general a type can be connected without being pointed.
  In \cref{sec:connectivity} we will define connectedness as the $n=0$ case of a general notion of $n$-connectedness, and in \cref{ex:connectivity-inductively} the reader is asked to show that this definition is equivalent to having both $\brck{A}$ and $\prd{x,y:A} \brck{x=y}$.
\end{rmk}

\begin{lem}\label{thm:contr-unit}
  For a type $A$, the following are logically equivalent.
  \begin{enumerate}
  \item $A$ is contractible in the sense of \cref{defn:contractible}.\label{item:contr}
  \item $A$ is a mere proposition, and there is a point $a:A$.\label{item:contr-inhabited-prop}
  \item $A$ is equivalent to \unit.\label{item:contr-eqv-unit}
  \end{enumerate}
\end{lem}
\begin{proof}
  If $A$ is contractible, then it certainly has a point $a:A$ (the center of contraction), while for any $x,y:A$ we have $x=a=y$; thus $A$ is a mere proposition.
  Conversely, if we have $a:A$ and $A$ is a mere proposition, then for any $x:A$ we have $x=a$; thus $A$ is contractible.
  And we showed~\ref{item:contr-inhabited-prop}$\Rightarrow$\ref{item:contr-eqv-unit} in \cref{thm:inhabprop-eqvunit}, while the converse follows since \unit easily has property~\ref{item:contr-inhabited-prop}.
\end{proof}

\begin{lem}\label{thm:isprop-iscontr}
  For any type $A$, the type $\iscontr(A)$ is a mere proposition.
\end{lem}
\begin{proof}
  Suppose given $c,c':\iscontr(A)$.
  We may assume $c\jdeq(a,p)$ and $c'\jdeq(a',p')$ for $a,a':A$ and $p:\prd{x:A} (a=x)$ and $p':\prd{x:A} (a'=x)$.
  By the characterization of paths in $\Sigma$-types, to show $c=c'$ it suffices to exhibit $q:a=a'$ such that $\trans{q}{p}=p'$.
  %
  We choose $q\defeq p(a')$.
  Now since $A$ is contractible (by $c$ or $c'$), by \cref{thm:contr-unit} it is a mere proposition.
  Hence, by \cref{thm:prop-set,thm:isprop-forall}, so is $\prd{x:A}(a'=x)$; thus $\trans{q}{p}=p'$ is automatic.
\end{proof}

\begin{cor}\label{thm:contr-contr}
  If $A$ is contractible, then so is $\iscontr(A)$.
\end{cor}
\begin{proof}
  By \cref{thm:isprop-iscontr} and \cref{thm:contr-unit}\ref{item:contr-inhabited-prop}.
\end{proof}

Like mere propositions, contractible types are preserved by many type constructors.
For instance, we have:

\begin{lem}\label{thm:contr-forall}
  If $P:A\to\type$ is a type family such that each $P(a)$ is contractible, then $\prd{x:A} P(x)$ is contractible.
\end{lem}
\begin{proof}
  By \cref{thm:isprop-forall}, $\prd{x:A} P(x)$ is a mere proposition since each $P(x)$ is.
  But it also has an element, namely the function sending each $x:A$ to the center of contraction of $P(x)$.
  Thus by \cref{thm:contr-unit}\ref{item:contr-inhabited-prop}, $\prd{x:A} P(x)$ is contractible.
\end{proof}

\index{function extensionality}%
(In fact, the statement of \cref{thm:contr-forall} is equivalent to the function extensionality axiom.
See~\cref{sec:univalence-implies-funext}.)

Of course, if $A$ is equivalent to $B$ and $A$ is contractible, then so is $B$.
More generally, it suffices for $B$ to be a \emph{retract} of $A$.
By definition, a \define{retraction}
\indexdef{retraction}%
\indexdef{function!retraction}%
is a function $r : A \to B$ such that there exists a function $s : B \to A$, called its \define{section},
\indexdef{section}%
\indexdef{function!section}%
and a homotopy $\epsilon:\prd{y:B} (r(s(y))=y)$; then we say that $B$ is a \define{retract}%
\indexdef{retract!of a type}
of $A$.

\begin{lem}\label{thm:retract-contr}
  If $B$ is a retract of $A$, and $A$ is contractible, then so is $B$.
\end{lem}
\begin{proof}
  Let $a_0 : A$ be the center of contraction.
  We claim that $b_0 \defeq r(a_0) : B$ is a center of contraction for $B$.
  Let $b : B$; we need a path $b = b_0$.
  But we have $\epsilon_b : r(s(b)) = b$ and $\contr_{s(b)} : s(b) = a_0$, so by composition
  \[ \opp{\epsilon_b} \ct \ap{r}{\contr_{s(b)}} : b = r(a_0) \jdeq b_0. \qedhere\]
\end{proof}

Contractible types may not seem very interesting, since they are all equivalent to \unit.
One reason the notion is useful is that sometimes a collection of individually nontrivial data will collectively form a contractible type.
An important example is the space of paths with one free endpoint.
As we will see in \cref{sec:identity-systems}, this fact essentially
encapsulates the based path induction principle for identity types.


\begin{lem}\label{thm:contr-paths}
  For any $A$ and any $a:A$, the type $\sm{x:A} (a=x)$ is contractible.
\end{lem}
\begin{proof}
  We choose as center the point $(a,\refl a)$.
  Now suppose $(x,p):\sm{x:A}(a=x)$; we must show $(a,\refl a) = (x,p)$.
  By the characterization of paths in $\Sigma$-types, it suffices to exhibit $q:a=x$ such that $\trans{q}{\refl a} = p$.
  But we can take $q\defeq p$, in which case $\trans{q}{\refl a} = p$ follows from the characterization of transport in path types.
\end{proof}

When this happens, it can allow us to simplify a complicated construction up to equivalence, using the informal principle that contractible data can be freely ignored.
This principle consists of many lemmas, most of which we leave to the reader; the following is an example.

\begin{lem}\label{thm:omit-contr}
  Let $P:A\to\type$ be a type family.
  \begin{enumerate}
  \item If each $P(x)$ is contractible, then $\sm{x:A} P(x)$ is equivalent to $A$.\label{item:omitcontr1}
  \item If $A$ is contractible with center $a$, then $\sm{x:A} P(x)$ is equivalent to $P(a)$.\label{item:omitcontr2}
  \end{enumerate}
\end{lem}
\begin{proof}
  In the situation of~\ref{item:omitcontr1}, we show that $\proj1:\sm{x:A} P(x) \to A$ is an equivalence.
  For quasi-inverse we define $g(x)\defeq (x,c_x)$ where $c_x$ is the center of $P(x)$.
  The composite $\proj1 \circ g$ is obviously $\idfunc[A]$, whereas the opposite composite is homotopic to the identity by using the contractions of each $P(x)$.

  We leave the proof of~\ref{item:omitcontr2} to the reader (see \cref{ex:omit-contr2}).
\end{proof}

Another reason contractible types are interesting is that they extend the ladder of $n$-types mentioned in \cref{sec:basics-sets} downwards one more step.

\begin{lem}\label{thm:prop-minusonetype}
  A type $A$ is a mere proposition if and only if for all $x,y:A$, the type $\id[A]xy$ is contractible.
\end{lem}
\begin{proof}
  For ``if'', we simply observe that any contractible type is inhabited.
  For ``only if'', we observed in \cref{subsec:hprops} that every mere proposition is a set, so that each type $\id[A]xy$ is a mere proposition.
  But it is also inhabited (since $A$ is a mere proposition), and hence by \cref{thm:contr-unit}\ref{item:contr-inhabited-prop} it is contractible.
\end{proof}

Thus, contractible types may also be called \define{$(-2)$-types}.
They are the bottom rung of the ladder of $n$-types, and will be the base case of the recursive definition of $n$-types in \cref{cha:hlevels}.

\index{type!contractible|)}%
\index{contractible!type|)}%

\sectionNotes

The fact that it is possible to define sets, mere propositions, and contractible types in type theory, with all higher homotopies automatically taken care of as in \cref{sec:basics-sets,subsec:hprops,sec:contractibility}, was first observed by Voevodsky.
In fact, he defined the entire hierarchy of $n$-types by induction, as we will do in \cref{cha:hlevels}.\index{n-type@$n$-type!definable in type theory}%

\cref{thm:not-dneg,thm:not-lem} rely in essence on a classical theorem of Hedberg,
\index{Hedberg's theorem}%
\index{theorem!Hedberg's}%
which we will prove in \cref{sec:hedberg}.
The implication that the propositions-as-types form of \LEM{} contradicts univalence was observed by Mart\'\i n Escard\'o on the \Agda mailing list.
The proof we have given of \cref{thm:not-dneg} is due to Thierry Coquand.

The propositional truncation was introduced in the extensional type theory of
\index{proof!assistant!\NuPRL}%
\NuPRL in 1983 by Constable~\cite{Con85} as an
application of ``subset'' and ``quotient'' types.  What is here called the
``propositional truncation'' was called ``squashing'' in the \NuPRL type theory~\cite{constable+86nuprl-book}.
Rules characterizing the propositional truncation directly, still in extensional type theory, were given in~\cite{ab:bracket-types}.
The intensional version in homotopy type theory was constructed by Voevodsky using an impredicative\index{impredicative!truncation} quantification, and later by Lumsdaine using higher inductive types (see \cref{sec:hittruncations}).

\index{propositional!resizing}%
Voevodsky~\cite{Universe-poly} has proposed resizing rules of the kind considered in \cref{subsec:prop-subsets}.
\index{axiom!of reducibility}\index{resizing}%
These are clearly related to the notorious \emph{axiom of reducibility} proposed by Russell in his and Whitehead's \emph{Principia Mathematica}~\cite{PM2}.\index{Russell, Bertrand}

The adverb ``purely'' as used to refer to untruncated logic is a reference to the use of monadic modalities to model effects in programming languages; see \cref{sec:modalities} and the Notes to \cref{cha:hlevels}.

There are many different ways in which logic can be treated relative to type theory.
For instance, in addition to the plain propositions-as-types logic described in \cref{sec:pat}, and the alternative which uses mere propositions only as described in \cref{subsec:logic-hprop}, one may introduce a separate ``sort'' of propositions, which behave somewhat like types but are not identified with them.
This is the approach taken in logic enriched type theory~\cite{aczel2002collection} and in some presentations of the internal languages of toposes\index{topos} and related categories (e.g.~\cite{jacobs1999categorical,elephant}), as well as in the proof assistant \Coq.\index{proof!assistant!Coq@\textsc{Coq}}
Such an approach is more general, but less powerful.
For instance, the principle of unique choice (\cref{sec:unique-choice}) fails in the category of so-called setoids in \Coq~\cite{Spiwack}, in logic enriched type theory~\cite{aczel2002collection}, and in minimal type theory~\cite{maietti2005toward}.\index{setoid}
Thus, the univalence axiom makes our type theory behave more like the internal logic of a topos;~see also \cref{cha:set-math}.\index{topos}

Martin-L\"of~\cite{martin2006100} provides a discussion on the history of axioms of choice.
Of course, constructive and intuitionistic mathematics has a long and complicated history, which we will not delve into here; see for instance~\cite{TroelstraI,TroelstraII}.

\sectionExercises

\begin{ex}\label{ex:equiv-functor-set}
  Prove that if $\eqv A B$ and $A$ is a set, then so is $B$.
\end{ex}

\begin{ex}\label{ex:isset-coprod}
  Prove that if $A$ and $B$ are sets, then so is $A+B$.
\end{ex}

\begin{ex}\label{ex:isset-sigma}
  Prove that if $A$ is a set and $B:A\to \type$ is a type family such that $B(x)$ is a set for all $x:A$, then $\sm{x:A} B(x)$ is a set.
\end{ex}

\begin{ex}\label{ex:prop-endocontr}
  Show that $A$ is a mere proposition if and only if $A\to A$ is contractible.
\end{ex}

\begin{ex}\label{ex:prop-inhabcontr}
  Show that $\eqv{\isprop(A)}{(A\to\iscontr(A))}$.
\end{ex}

\begin{ex}\label{ex:lem-mereprop}
  Show that if $A$ is a mere proposition, then so is $A+(\neg A)$.
  Thus, there is no need to insert a propositional truncation in~\eqref{eq:lem}.
\end{ex}

\begin{ex}\label{ex:disjoint-or}
  More generally, show that if $A$ and $B$ are mere propositions and $\neg(A\times B)$, then $A+B$ is also a mere proposition.
\end{ex}

% \begin{ex}\label{ex:hprop-iff-equiv}
%   Show that if $A$ and $B$ are mere propositions such that $A\to B$ and $B\to A$, then $\eqv A B$.
% \end{ex}

% \begin{ex}\label{ex:isprop-isprop}
%   Show that for any type $A$, the types $\isprop(A)$ and $\isset(A)$ are mere propositions.
% \end{ex}

% \begin{ex}\label{ex:prop-eqvtrunc}
%   Show that if $A$ is already a mere proposition, then $\eqv A{\brck{A}}$.
% \end{ex}

\begin{ex}\label{ex:brck-qinv}
  Assuming that some type $\isequiv(f)$ satisfies conditions~\ref{item:be1}--\ref{item:be3} of \cref{sec:basics-equivalences}, show that the type $\brck{\qinv(f)}$ satisfies the same conditions and is equivalent to $\isequiv(f)$.
\end{ex}

\begin{ex}\label{ex:lem-impl-prop-equiv-bool}
  Show that if \LEM{} holds, then the type $\prop \defeq \sm{A:\type} \isprop(A)$ is equivalent to \bool.
\end{ex}

\begin{ex}\label{ex:lem-impred}
  Show that if $\UU_{i+1}$ satisfies \LEM{}, then the canonical inclusion $\prop_{\UU_i} \to \prop_{\UU_{i+1}}$ is an equivalence.
\end{ex}

\begin{ex}\label{ex:not-brck-A-impl-A}
  Show that it is not the case that for all $A:\type$ we have $\brck{A} \to A$.
  (However, there can be particular types for which $\brck{A}\to A$.
  \cref{ex:brck-qinv} implies that $\qinv(f)$ is such.)
\end{ex}

\begin{ex}\label{ex:lem-impl-simple-ac}
  \index{axiom!of choice}%
  Show that if \LEM{} holds, then for all $A:\type$ we have $\bbrck{(\brck A \to A)}$.
  (This property is a very simple form of the axiom of choice, which can fail in the absence of \LEM{}; see~\cite{krausgeneralizations}.)
\end{ex}

\begin{ex}\label{ex:naive-lem-impl-ac}
  We showed in \cref{thm:not-lem} that the following naive form of \LEM{} is inconsistent with univalence:
  \[ \prd{A:\type} (A+(\neg A)) \]
  In the absence of univalence, this axiom is consistent.
  However, show that it implies the axiom of choice~\eqref{eq:ac}.
\end{ex}

\begin{ex}\label{ex:lem-brck}
  Show that assuming \LEM{}, the double negation $\neg \neg A$ has the same recursion principle as the propositional truncation $\brck A$ but with a propositional computation rule rather than a judgmental one.
  In other words, prove that assuming \LEM{}, if $B$ is a mere proposition and we have $f:A\to B$, then there is an induced $g:\neg\neg A \to B$ such that $g(\bproj a) = f(a)$ for all $a:A$.
  Deduce that (assuming \LEM{}) we have $\eqv{\neg\neg A}{\brck{A}}$.
  Thus, under \LEM{}, the propositional truncation can be defined rather than taken as a separate type former.
\end{ex}

\begin{ex}\label{ex:impred-brck}
  \index{propositional!resizing}%
  Show that if we assume propositional resizing as in \cref{subsec:prop-subsets}, then the type
  \[\prd{P:\prop} \Parens{(A\to P)\to P}\]
  has the same recursion principle as $\brck A$, \emph{with} the same judgmental computation rule.
  Thus, we can also define the propositional truncation in this case.
\end{ex}

\begin{ex}\label{ex:lem-impl-dn-commutes}
  Assuming \LEM{}, show that double negation commutes with universal quantification of mere propositions over sets.
  That is, show that if $X$ is a set and each $Y(x)$ is a mere proposition, then \LEM{} implies
  \begin{equation}
    \eqv{\Parens{\prd{x:X} \neg\neg Y(x)}}{\Parens{\neg\neg \prd{x:X} Y(x)}}.\label{eq:dnshift}
  \end{equation}
  Observe that if we assume instead that each $Y(x)$ is a set, then~\eqref{eq:dnshift} becomes equivalent to the axiom of choice~\eqref{eq:epis-split}.
\end{ex}

\begin{ex}\label{ex:prop-trunc-ind}
  \index{induction principle!for truncation}%
  Show that the rules for the propositional truncation given in \cref{subsec:prop-trunc} are sufficient to imply the following induction principle: for any type family $B:\brck A \to \type$ such that each $B(x)$ is a mere proposition, if for every $a:A$ we have $B(\bproj a)$, then for every $x:\brck A$ we have $B(x)$.
\end{ex}

\begin{ex}\label{ex:lem-ldn}
  Show that the law of excluded middle~\eqref{eq:lem} and the law of double negation~\eqref{eq:ldn} are logically equivalent.
\end{ex}

\begin{ex}\label{ex:decidable-choice}
  Suppose $P:\nat\to\type$ is a decidable family (see \cref{defn:decidable-equality}\ref{item:decidable-equality2}) of mere propositions.
  Prove that
  \[ \Brck{\sm{n:\nat} P(n)} \;\to\; \sm{n:\nat}P(n).\]
\end{ex}

\begin{ex}\label{ex:omit-contr2}
  Prove \cref{thm:omit-contr}\ref{item:omitcontr2}: if $A$ is contractible with center $a$, then $\sm{x:A} P(x)$ is equivalent to $P(a)$.
\end{ex}

\begin{ex}\label{ex:isprop-equiv-equiv-bracket}
  Prove that $\isprop(P) \simeq (P \simeq \brck P)$.
\end{ex}

\begin{ex}\label{ex:finite-choice}
  As in classical set theory, the finite version of the axiom of choice is a theorem.  Prove that the axiom of choice \eqref{eq:ac} holds when $X$ is a finite type $\Fin(n)$ (as defined in \cref{ex:fin}).
\end{ex}

\begin{ex}\label{ex:decidable-choice-strong}
  Show that the conclusion of \cref{ex:decidable-choice} is true if $P:\nat\to\type$ is any decidable family.
\end{ex}

\begin{ex}\label{ex:n-set}
  Simplify the proof of \cref{thm:path-nat} by first proving that $\code(m,n)$ is a mere proposition for all $m,n$.
\end{ex}

% Local Variables:
% TeX-master: "hott-online"
% End: