intro-uf.tex

  %% this chapter sets up the foundational system, which is Univalent Foundations
\chapter{An introduction to univalent mathematics}
\label{ch:univalent-mathematics}

\section{What is a type?}
\label{sec:what-is-a-type}

In some computer programming languages, all variables are introduced along with a declaration of the type of thing they will refer to.  Knowing
the type of thing a variable refers to allows the computer to determine which expressions in the language are \emph{grammatically well
formed}\footnote{The grammar of a programming language consists of all the language's rules.  A statement or expression in a programming
language is grammatically well formed if it follows all the rules.}, and hence valid.  For example, if $s$ is a
string\footnote{A \emph{string} is a sequence of characters, such as ``qwertyuiop''.} and $x$ is a real number, we may write $1/x$, but we may not write $1/s$.%
\footnote{In a programming language, the well formed expression $1/x$ may produce a run-time error if $x$ happens to have the value $0$.}

To enable the programmer to express such declarations, names are introduced to refer to the various types of things.  For example, the name
$\bool$ may be used to declare that a variable is a Boolean value\footnote{A Boolean value is either \emph{true} or \emph{false}.},
  $\integer$ may refer to 32-bit integers, and $\real$ may refer to 64-bit floating point numbers\footnote{An example of a \emph{floating
point number} is $.625 \times 2^{33}$ -- the \emph{mantissa} $.625$ and the \emph{exponent} $33$ are stored inside the floating point number.
The ``point'', when the number is written in base $2$ notation, is called ``floating'', because its position is easily changed by modifying the exponent.}.

Types occur in mathematics, too, and are used in the same way: all variables are introduced along with a declaration of the type of thing they
will refer to.\index{type} For example, one may say ``consider a real number $x$'', ``consider a natural number $n$'', ``consider a point $P$ of
the plane'', or ``consider a line $L$ of the plane''.  After that introduction, one may say that the \emph{type} of $n$ is \emph{natural number} and
that the \emph{type} of $P$ is \emph{point of the
plane}.  Just as in a computer program, type declarations such as those are used to determine which mathematical statements are grammatically
well formed.  Thus one may write ``$P$ lies on $L$'' or $1/x$, but not ``$L$ lies on $P$'' nor $1/L$.\footnote{In mathematics there are no
``run-time'' errors; rather, it is legitimate to write the expression $1/x$ only if we already know that $x$ is a non-zero real number.}

Often ordinary English writing is good enough for such declarations in mathematics expositions, but, for convenience, mathematicians usually
introduce symbolic names to refer to the various types of things under discussion.  For example, the name $\NN$ is usually used when declaring
that a variable is a natural number, the name $\ZZ$ is usually used when declaring that a variable is an integer, and the name $\RR$ is usually
used when declaring that a variable is a real number.  Ways are also given for constructing new type names from old ones: for example, the name
$\RR\times\RR$ may be used when declaring that a variable is a point of the plane, for it conveys the information that a point of the plane is a
pair of real numbers.

Once one becomes accustomed to the use of names such as $\NN$ in mathematical writing and speaking, it is natural to take the next step and
regard those names as denoting things that exist.  Thus, we shall refer to $\NN$ as the \emph{type of all natural numbers}, and we will think of
it as a mathematical object in its own right.  Intuitively and informally, it is a collection whose members (or \emph{elements}) are the natural
numbers.

Once we view the various types as existing as mathematical objects, they become worthy of study.  The language of mathematics is thereby
improved, and the scope of mathematics is broadened.  For example, we can consider statements such as ``$\NN$ is infinite'' and to try to prove
it.

Historically, there was some hesitation\footnote{TO DO : Include some pointers to discussions of potential infinity and actual infinity, perhaps.} about
introducing the collection of all natural numbers as a mathematical object, perhaps because if one were to attempt to build the collection from
nothing by adding numbers to it one at a time, it would take an eternity to complete the assembly.  We won't regard that as an obstacle.

We have said that the types of things are used to determine whether mathematical statements are well formed.
Therefore, if we expect ``$\NN$ is infinite'' to be a well-formed statement, we'll have to know what type of thing $\NN$ is, and we'll
have to have a name for that type.  Similarly, we'll have to know what type of thing that type is, and we'll have to have a name for it,
and so on forever.  Indeed, all of that is part of what will be presented in this chapter.

\section{Types, elements, families, and functions}
\label{univalent-mathematics}

In this section we build on the intuition imparted in the previous section.

In \emph{univalent mathematics},\index{mathematics!univalent}\footnote{The term ``univalent'' is a word coined by Vladimir Voevodsky, who
introduced it to describe his principle that types that are \emph{equivalent} in a certain sense can be identified with each other.  The
principle is stated precisely in \cref{def:univalence}.  As Voevodsky explained, the word comes from a Russian translation of a mathematics
book, where the English mathematical term ``faithful'' was translated into Russian as the Russian word that sounds like ``univalent''.  He also
said ``Indeed these foundations seem to be faithful to the way in which I think about mathematical objects in my head.''} types are used to
classify all mathematical objects.  Every mathematical object is an \emph{element} (or a \emph{member}) of some \emph{type}.  Before
one can talk about an object of a certain type, one must introduce the type itself.  There are enough ways to form new types from old ones to
provide everything we need to write mathematics.

One expresses the declaration that an object $a$ is an element of the \emph{type} $X$ by writing $a:X$.%
\footnote{The notation in mathematics based on \emph{set theory} that corresponds (sort of) to this is $a \in X$.}
\index{element}
\glossary(2:){${:}$}{element judgment}

Using that notation, each variable $x$ is introduced along with a declaration of the form $x:X$, which declares that $x$ will refer to something
of type $X$, but provides no other information about $x$.  The declared types of the variables are used to determine which statements of the
theory are grammatically well formed.

After introducing a variable $x:X$, it may be possible to form an expression $T$ representing a type, all of whose components have
already been given a meaning.
(Here the variable $x$ is regarded also as having already been given a meaning, even though the only thing known about it is its type.)
To clarify the dependence of $T$ on $x$ primarily, we may write $T(x)$ (or $T_x$) instead of $T$.
Such an expression will be called a \emph{family of types} \index{family!of types} parametrized by the variable $x$ of type $X$.
Such a family provides a variety of types, for, if $a$ is any expression denoting an object of $X$, one may replace all
occurrences of $x$ by $a$ in $T$, thereby obtaining a new expression representing a type, which may be regarded as a \emph{member}
and which may be denoted by $T(a)$.

Naturally, if the expression $T$ doesn't actually involve the variable $x$, then the members of the family are all the same,
and we'll refer to the family as a \emph{constant family} of types.

Here's an example of a family of types: let $T$ be the type
of all natural numbers greater than $2$. For any element $n$ of $T$
we let $P_n$ be the type of $n$-sided polygons in the plane.
It gives a family of types parametrized by the elements of $T$.%
\footnote{\color{casred} See if you like my solution. If so, remove footnote.}
One of the members of the family is the type $P_5$ of all pentagons in the plane.

A family of types may be parametrized by more than one variable.  For example, after introducing a variable $x:X$ and a family of types $T$
parametrized by $x$, we may introduce a variable $t:T$.  Then it may be possible to form an expression $S$ representing a type that involves the
variables $x$ and $t$.  Such an expression will be called a family of types parametrized by $x$ and $t$, and we may write $S(x,t)$ instead of
$S$ to emphasize the dependence on $x$ and $t$.  The same sort of thing works with more variables.

After introducing a variable $x:X$ and a family of types $T$, it may be possible to form an expression $e$ of type $T$, all of whose components have already been
given a meaning.
Such an expression will also be called a \emph{family of elements of $T$} \index{family!of elements} parametrized by the elements of $X$, when
we wish to focus on the dependence of $e$ (and perhaps $T$) on the variable $x$.
To clarify the dependence of $e$ on $x$ primarily, we may write $e(x)$ (or $e_x$) instead of $e$.
Such a family provides a variety of elements of members of the family $T$, for, if $a$ is any expression denoting an object of $X$, one may replace all
occurrences of $x$ by $a$ in $e$ and in $T$, thereby obtaining an element of $T(a)$, which may be regarded as a \emph{member} of the family $e$
and which will be denoted by $e(a)$.

Naturally, if the expressions $e$ and $T$ don't actually involve the variable $x$, then the members of the family are all the same,
and we'll refer to the family as a \emph{constant family} of elements.

Here's an example of a family of elements in a constant family of types: we let $n$ be a natural number and consider the real number $\sqrt n$.
It gives a family of real numbers parametrized by the natural numbers.
(The family may also be called a \emph{sequence} of real numbers).
One of the members of the family is $\sqrt{11}$.

Here's an example of a family of elements in a (non-constant) family of types.
As above, let $T$ be the type of all natural numbers greater than $2$ and let
$P_n$ be the type of $n$-sided polygons in the plane, for any $n:T$.
Now consider the regular $n$-sided polygon $p_n$ of radius $1$ with
a vertex on the positive $x$-axis, for any $n:T$.  We see that $p_n : P_n$.
One of the members of this family of \emph{elements} $p_n$ is the regular
pentagon $p_5$ of radius $1$ with a vertex on the positive $x$-axis.
The pentagon $p_5$ is an element of the type $P_5$, which is a member of the
family of \emph{types} $P_n$ ($n:T$). In short, $5:T$ and $p_5 : P_5$.

The type $X$ containing the variable for a family of types or a family of elements is called the \emph{parameter type}\index{parameter type} of
the family.

Just as a family of types may depend on more than one variable, a family of elements may also depend on more than one variable.

Families of elements can be enclosed in mathematical objects called \emph{functions}\index{function} (or \emph{maps}\index{map}), as one might
expect.
Let $e$ be a family of elements of a family of types $T$,
both of which are parametrized by the elements $x$ of $X$.  We use the notation $x \mapsto e$ for the function that sends an element $a$ of $X$
to the element $e(a)$ of $T(a)$; the notation $x \mapsto e$ can be read as ``$x$ maps to $e$'' or ``$x$ goes to $e$''.  (Recall that $e(a)$ is
the expression that is obtained from $e$ by replacing all occurrences of $x$ in $e$ by $a$.)  If we name the function $f$, then that element of
$T$ will be denoted by $f(a)$.  The \emph{type} of the function $x \mapsto e$ is called a \emph{product type} and will be denoted by
$\prod_{x:X} T(x)$.\index{product type}\glossary(916Pi){$\prodop_{x:X}T(x)$}{product type of dependent functions}
If $T$ is a constant family of types, then the type will also be
called a \emph{function type} and will be denoted by $X \to T$\glossary(2fun){$\protect\to$}{function type}.  Thus when we write $f : X \to T$,
we mean that $f$ is an element of the type $X \to T$, and we are saying that $f$ is a function from $X$ to $T$.  The type $X$ may be called the
\emph{domain} of $f$, and the type $T$ may be called the \emph{codomain} of $f$.

An example of a function is the function $n \mapsto \sqrt n$ of type $\NN \to \RR$.

Another example of a function is the function $n \mapsto p_n$ of type $\prod_{n:\NN} P_n$, where $P_n$ is the type of polygons introduced above,
and $p_n$ is the polygon introduced above.

Another example of a function is the function $m \mapsto (n \mapsto m+n)$ of type $\NN \to (\NN \to \NN)$.  It is a function that accepts a
natural number as argument and returns a function as its value.  The function returned is of type $\NN \to \NN$.  It accepts a natural number
as argument and returns a natural number as value.

The reader may wonder why the word ``product'' is used when speaking of product types.  To motivate that, we consider a simple example
informally.  We take $X$ to be a type with just two elements, $b$ and $c$.  We take $T(x)$ to be a family of types parametrized by the elements
of $X$, with $T(b)$ being a type with $5$ elements and $T(c)$ being a type with $11$ elements.  Then the various functions $f$ of type
$\prod_{x:X} T(x)$ are plausibly obtained by picking a suitable element for $f(b)$ from the $5$ possibilities in $T(b)$ and by picking a
suitable element for $f(c)$ from the $11$ possibilities in $T(c)$.  The number of ways to make both choices is $5 \times 11$, which is a
\emph{product} of two numbers.  Thus $\prod_{x:X} T(x)$ is sort of like the product of $T(b)$ and $T(c)$, at least as far as counting is
concerned.

The reader may wonder why we bother with functions at all: doesn't the expression $e$ serve just as well as the function $x \mapsto e$, for all
practical purposes?  The answer is no.  One reason is that the expression $e$ doesn't inform the reader that the variable under consideration is
$x$.  Another reason is that we may want to use the variable $x$ for elements of a different type later on: then $e(x)$ is no longer well
formed.  For example, imagine first writing this: ``For a natural number $n$ we consider the real number $\sqrt n$'' and then writing this:
``Now consider a triangle $n$ in the plane.''  The result is that $\sqrt n$ is no longer usable, whereas the function $n \mapsto \sqrt n$ has
enclosed the variable and the family into a single object and remains usable.\footnote{Students of trigonometry are already familiar with the
concept of function, as something enclosed this way.  The sine and cosine functions, $\sin$ and $\cos$, are examples.}

Once a family $e$ has been enclosed in the function $x \mapsto e$, the variable $x$ is referred to as a \emph{dummy variable}\index{dummy
  variable} or as a \emph{bound variable}\index{bound variable}.\footnote{Students of calculus are familiar with the concept of dummy variable
and are accustomed to using identities such as $\int_a^b f(t)\,dt = \int_a^b f(x)\,dx$.} This signifies that the name of the variable no longer
matters, in other words, that $x \mapsto e(x)$ and $t \mapsto e(t)$ may regarded as identical.  Moreover, the variable $x$ that occurs inside
the function $x \mapsto e$ is regarded as unrelated to variables $x$ which may appear elsewhere in the discussion.

If the variable $x$ in our notation $x \mapsto e(x)$ is a dummy variable, and its name doesn't matter, then we may consider the possibility of
not specifying a variable at all.  We introduce now a methodical way to do that, by replacing the occurrences of the variable $x$ in the
expression $e(x)$ by an \emph{underscore},\index{underscore}
yielding $e(\blank)$ as alternative notation for the function $x \mapsto e(x)$.
For example, the
notation $\sqrt{\vphantom{n}\blank}$ can serve as alternative notation for the function $n \mapsto \sqrt n$ introduced above, and $2 + \blank$ can serve as
alternative notation for the function $n \mapsto 2 + n$ of type $\NN \to \NN$.

We have mentioned above the possibility of giving a name to a function.
We expand on that now by introducing notation for making and for using \emph{definitions}.\index{definition}

The notation $x \defeq z$ will be an announcement that we are defining
the expression $x$ to be the expression $z$, all of whose components have already been given a meaning;
in that case, we will say that $x$ has been \emph{defined} to be (or to mean) $z$.%
\glossary(2:=){$\protect\defeq$}{definition}
The forms allowed for the expression $x$ will be made clear by the examples we give.

For example, after writing $n \defeq 12$, we will say that $n$ has
been defined to be $12$.

For another example, naming the function $x \mapsto e(x)$ as $f$
(as we did above) can be done by writing $f \defeq ( x \mapsto e(x) )$.
Alternatively and more traditionally, we may write $f(x) \defeq e(x)$.
Both mean that $f$ has been defined to be $x \mapsto e(x)$
and that, consequently, $f(a)$ has been defined to be $e(a)$,
for any element $a$ of $X$.

The notation $b \jdeq c$ will denote the statement that the expressions $b$ and $c$ become the same thing if all the subexpressions within $b$
or $c$ are expanded according to their definitions, if any; in that case, we will say that $b$ and $c$ are \emph{the same by
definition}\glossary(2==){$\jdeq$}{equality by definition}.  For example, after writing $n \defeq 12$ and $m \defeq n$, we may say that $j + 12
\jdeq j + m$ and that $m \times 11 \jdeq 12 \times 11$.

Whenever two expressions are the same by definition, we may replace one with the other inside any other expression, because the expansion of
definitions is regarded as trivial and transparent.

We proceed now to the promised example.  Consider functions $f : X \to Y$ and $g : Y \to Z$.  We define the \emph{composite} function
$g \circ f : X \to Z$ by setting $g \circ f \defeq (a \mapsto g(f(a)))$.\glossary(2fundef){$\mapsto$}{``maps to'', function definition}\index{composition!of functions}
In other words, it
is the function that sends an arbitrary element $a$ of $X$ to $g(f(a))$ in $Z$.  (The expression $g \circ f$ may be read as ``$g$ circle $f$''
or as ``$g$ composed with $f$''.)  The composite function $g \circ f$ may also be denoted simply by $gf$.\glossary(2circ){$\circ$}{function composition}

Now consider functions $f : X \to Y$, $g : Y \to Z$, and $h : Z \to W$.  Then $(h \circ g) \circ f$ and $h \circ (g \circ f)$ are the same by
definition, since applying the definitions within expands both expressions to $a \mapsto h(g(f(a)))$.  In other
words, we have established that $(h \circ g) \circ f \jdeq h \circ (g \circ f)$.  Thus, we may write $h \circ g \circ f$ for
either expression, without danger of confusion.

One may define the identity function $\id_X : X \to X$ by setting
$\id_X \defeq (a \mapsto a)$.\index{function!identity}
\glossary(id){$\id$}{identity function} Application of definitions shows that
$f \circ \id_X$ is the same by definition as $a \mapsto f(a)$, which, by a standard convention, which we adopt\footnote{The convention that
  $f \jdeq (a \mapsto f(a))$ is referred to as the \emph{$\eta$-rule}\glossary(907-rule){$\eta$}{$\eta$-rule} in the jargon of type theory.}, is to be regarded as the same as $f$.  In
other words, we have established that $f \circ \id_X \jdeq f$.%
\phantomsection\label{page:idofetaf}
A similar computation applies to $\id_Y \circ f$.

In the following sections we will present various other elementary types and elementary ways to make new types from old ones.

\section{Universes}
\label{sec:universes}

In~\cref{univalent-mathematics} we have introduced the objects known as \emph{types}.  They have \emph{elements}, and the type an
element belongs to determines the type of thing that it is.  At various points in the sequel, it will be convenient for types also to be
elements, for that will allow us, for example, to enclose families of types in functions.  To achieve this
convenience, we introduce types that are \emph{universes}.  Some care is required, for the first temptation is to posit a
single new type $\UU$ called \emph{the universe}, so that every type is realized as an element of $\UU$.  This universe would be ``the type of
all types'', but introducing it would lead to an absurdity, for roughly the same reason that introduction of a ``set of all sets'' leads to the absurdity
in traditional mathematics known as Russell's paradox.\footnote{%
  In fact, type theory can trace its origins to Russell's paradox,
  announced in a 1902 letter to Frege as follows:\\
  \begin{adjustwidth}{\parindent}{}
    There is just one point where I have encountered a difficulty.
    You state that a function too, can act as the indeterminate element.
    This I formerly believed,
    but now this view seems doubtful to me because of the following contradiction.
    Let $w$ be the predicate: to be a predicate that cannot be predicated of itself.
    Can $w$ be predicated of itself? From each answer its opposite follows.
    Therefore we must conclude that $w$ is not a predicate.
    Likewise there is no class (as a totality) of those classes which,
    each taken as a totality, do not belong to themselves.
  \end{adjustwidth}
  To which Frege replied:
  \begin{adjustwidth}{\parindent}{}
  Incidentally, it seems to me that the expression
  ``a predicate is predicated of itself'' is not exact.
  A predicate is as a rule a first-level function,
  and this function requires an object as argument
  and cannot have itself as argument (subject).
  \end{adjustwidth}
  Russell then quickly added \emph{Appendex~B} to his
  \emph{Principles of Mathematics} (1903), in which he said that
  ``it is the distinction of logical types that is the key to the whole mystery'',
  where types are the \emph{ranges of significance} of variables.
  For more on the history of type theory,
  see~\citeauthor{sep-type-theory}\footnotemark{}.}\footcitetext{sep-type-theory}
  Some later approaches to set theory included the notion of a \emph{class}, with the collection of all sets being the primary example of a class.
  Classes are much like sets, and every set is a class, but not every class is a set.
  Then one may wonder what sort of thing the collection of all classes would be.  Such
  musings are resolved in univalent mathematics as follows.

\begin{enumerate}
  \item There are some types called \emph{universes}.\index{universe}\glossary(UU){$\protect\UU$}{universe}
  \item If $\UU$ is a universe, and $X : \UU$ is an element of $\UU$, then $X$ is a type.
  \item If $X$ is a type, then it appears as an element in some
  universe $\UU$. Moreover, if $X$ and $Y$ are types,
  then there is a universe $\UU$ containing both of them.
  This universe $\UU$ also contains the type $X\to Y$ and similar
  types constructed from $X$ and $Y$.
  \item\label{it:cumulative} If $\UU$ and $\UU'$ are universes,
  $\UU:\UU'$, $X$ is a type, and $X:\UU$, then also $X:\UU'$.
  (Thus we may regard $\UU'$ as being \emph{larger} than $\UU$.)
  \item There is a particular universe $\UU_0$, which we single out to serve
  as a repository for certain basic types to be introduced in the sequel.
  Moreover, $\UU_0 : \UU$ for every other universe $\UU$,
  and thus $\UU_0$ is the \emph{smallest} universe.
\end{enumerate}

It follows from the properties above that there are an infinite number of
 universes, for each one is an element of a larger one. For the sake of
 clarity, throughout this book, we use an infinite sequence of universes
 $\UU_0 : \UU_1 : \UU_2 : \dots$.

Now suppose we have a type $X$ and a family $T(x)$ of types parametrized by a variable $x$ of type $X$.  Choose a universe $\UU$ with $T(x) : \UU$.
Then we can make a function of type $X \to \UU$, namely $f \defeq (x \mapsto T(x))$.  Conversely, if $f'$ is a function of type $X \to \UU$, then
we can make a family of types parametrized by $x$, namely $T' \defeq f'(x)$.  The flexibility offered by this correspondence between families of
types in $\UU$ and functions to $\UU$ will often be used.

\section{The type of natural numbers}
\label{sec:natural-numbers}

Here are Peano's rules\footcite{peano-principia} for constructing the natural numbers in the form that is used in type theory.
\begin{enumerate}[label=(P\arabic*),ref=(P\arabic*)]
\item\label{P1} there is a type called $\NN$ in the universe $\UU_0$
  (whose elements will be called \emph{natural numbers});%
  \glossary(N){$\protect\NN$}{the type of natural numbers, Peano's rules, \cref{P1}}
\item\label{P2} there is an element of $\NN$ called $0$, called \emph{zero};%
  \glossary(80){$0$}{the natural number zero, Peano's rules, \cref{P2}}\index{zero}
\item\label{P3} if $m$ is a natural number, then there is also a natural number $\Succ(m)$, called the \emph{successor} of $m$;%
  \glossary(succ){$\protect\Succ$}{the successor function on $\NN$, Peano's rules, \cref{P3}}%
  \index{successor}
\item\label{P4} suppose we are given:
  \begin{enumerate}
  \item a family of types $X(m)$ parametrized by a variable $m$ of type $\NN$;
  \item an element $a$ of $X(0)$; and
  \item a family of functions $g_m : X(m) \to X(\Succ(m))$.
  \end{enumerate}
  Then from those data we are provided with a family of elements $f(m) : X(m)$,
  satisfying $f(0) \jdeq a$ and $f(\Succ(m)) \jdeq g_m(f(m))$.
\end{enumerate}

The first three rules present few problems for the reader.  They provide us with the smallest natural number $0:\NN$, and we may introduce as
many others as we like with the following definitions.
\begin{align*}
  1 & \defeq \Succ(0) \glossary(81){$1$}{the natural number 1} \\
  2 & \defeq \Succ(1) \glossary(82){$2$}{the natural number 2} \\
  3 & \defeq \Succ(2) \glossary(83){$3$}{the natural number 3} \\
  & \quad \vdots
\end{align*}

You may recognize rule \ref{P4} as ``the principle of mathematical induction''.\footnote{%
  Rule \ref{P4} and our logical framework are stronger than in Peano's original formulation, and this allows us to omit some rules that Peano had to include:
  that different natural numbers have different successors; and that no number has $0$ as its successor.  Those omitted rules
  remain true in this formulation and can be proved from the other rules, after we have introduced the notion of equality in
  our logical framework.}
We will refer to it simply as ``induction on $\NN$''.

You may also recognize the function $f$ in \ref{P4} as ``defined by recursion''.
The point of the induction principle is that the type $X(m)$ of
$f(m)$ may depend on $m$. An important special case is when $X(m)$
does not depend on $m$, that is, when $X(m)\defeq Y$ for some type Y.
In this non-dependent case we refer to the principle as
``the recursion principle for $\NN$''. In other words, throughout
this book, the difference between an induction principle and the
corresponding recursion principle is that in the latter principle
the type family is constant.
\index{principle!induction}\index{induction principle}
\index{principle!recursion}\index{recursion principle}


The resulting family $f$ may be regarded as having been defined inductively
by the two declarations $f(0) \defeq a$ and $f(\Succ(m)) \defeq g_m(f(m))$,
and indeed, we will often simply write such a pair of declarations as a shorthand way of applying rule \ref{P4}.
The two declarations cover the two ways of introducing elements of $\NN$ via the use of the two rules \ref{P2} and \ref{P3}.
(In terms of computer programming, those two declarations amount to the code for a recursive subroutine that can handle any incoming natural number.)

With that notation in hand, speaking informally, we may regard \ref{P4} above as defining the family $f$ by the following infinite sequence of definitions.
\begin{align*}
  f(0) & \defeq a \\
  f(1) & \defeq g_0(a) \\
  f(2) & \defeq g_1(g_0(a)) \\
  f(3) & \defeq g_2(g_1(g_0(a))) \\
  & \quad \vdots
\end{align*}
(The need for the rule \ref{P4} arises from our inability to write down an infinite sequence of definitions in a finite amount of space, and
from the need for $f(m)$ to be defined when $m$ is a variable of type $\NN$, and thus is not known to be equal to $0$, nor to $1$, nor to $2$,
etc.)

We may use induction on $\NN$ to define of \emph{iteration} of functions.  Let $Y$ be a type, and suppose we have a function $e : Y \to Y$.  We
define by induction on $\NN$ the $m$-fold \emph{iteration} $e^m : Y \to Y$ by setting $e^0 \defeq \id_Y$ and $e^{\Succ(m)}\defeq e\circ e^m$.
(Here we apply rule \ref{P4} with the the type $Y \to Y$ as the family of types $X(m)$, the identity function $\id_Y$ for $a$, and the function
$d \mapsto e\circ d$ for the family $g_m : (Y\to Y)\to(Y\to Y)$ of functions.)

We may now define addition of natural numbers by induction on $\NN$.  For natural numbers $n$ and $m$ we define $n+m : \NN$ by induction on
$\NN$ with respect to the variable $m$ by setting $n+0\defeq n$ and $n+\Succ(m)\defeq \Succ(n+m)$.  (The reader should be able to extract the
family $X(m)$, the element $a$, and the family of functions $g_m$ from that pair of definitions.)  Application of definitions shows, for
example, that $2+2$ and $4$ are the same by definition, and thus we may write $2+2 \jdeq 4$, because both expressions reduce to
$\Succ(\Succ(\Succ(\Succ(0))))$.

Similarly we define the product $m \cdot n : \NN$ by induction on $m$ by setting setting $ 0 \cdot n \defeq 0$ and
$ \Succ(m) \cdot n \defeq (m \cdot n) + n$.

Alternatively (and equivalently) we may use iteration of functions to define addition and multiplication, by setting $n+m \defeq \Succ^m(n)$ and
$m \cdot n \defeq ( i \mapsto i + n )^m (0) $.

Finally, we may define the factorial function%
\index{factorial function}\index{function!factorial}
$\fact : \NN \to \NN$ by induction on $\NN$, setting $\fact(0) \defeq 1$ and
$\fact(\Succ(m)) \defeq \Succ(m) \cdot \fact(m)$.  (One can see that this definition applies rule \ref{P4} with $X(m) \defeq \NN$, with $1$ for
$a$, and with the function $n \mapsto \Succ(m) \cdot n$ for $g_m$.)  Application of the definitions shows, for example, that $\fact(3) \jdeq 6$, as
the reader may verify.

\section{Identity types}
\label{sec:identity-types}

One of the most important types is the \emph{identity type},
which implements a notion of equality.
Identity types are formed of a type and two elements of that type;
we shall have no need to compare elements of different types.

Here are the rules for constructing and using identity types.
\begin{enumerate}[label=(E\arabic*),ref=(E\arabic*)]\label{rules-for-equality}
  \item\label{E1}
    for any type $X$ and for any elements $a$ and $b$ of it, there is an \emph{identity type} $a \eqto b$;%
    \glossary(2=){$\xrightarrow =$}{identity type, \cref{E1}}%
    \index{identity type}
    moreover, if $X$ is an element of a universe $\UU$, then so is $a \eqto b$.
    \marginnote{When the type of $a$ and $b$ is not clear
    we may clarify it by writing $a \eqto_X b$.}
  \item\label{E2} for any type $X$ and for any element $a$ of it, there is an element $\refl a$ of type $a \eqto a$
    (the name $\refl{}$ comes from the word ``reflexivity'')%
    \glossary(refl){$\protect\refl{a}$}{reflexivity, identity type, \cref{E2}}
  \item\label{E3} suppose we are given:
    \begin{enumerate}
    \item a type $X$ and an element $a:X$;
    \item a family of types $P(b,e,\dots)$ parametrized by a variable $b$ of type $X$, a variable $e$ of type $a \eqto b$, and perhaps some
      further variables; and
    \item an element $p$ of $P(a,\refl a,\dots)$.
    \end{enumerate}
    Then from those data we are provided with a family of elements $f(b,e,\dots) : P(b,e,\dots)$.
    Moreover, $f(a,\refl a,\dots) \jdeq p$.
\end{enumerate}

We will refer to an element $i$ of $a \eqto b$ as an
\emph{identification} of $a$ with $b$.
Since the word ``identification'' is a long one,
we may also refer to $i$ as a \emph{path} from $a$ to
$b$ -- this has the advantage of incorporating the intuition that an identification may proceed gradually through intermediate steps.%
\index{identification}

The need to record, using the element $i$, the way we identify $a$
with $b$ may come as a surprise, since normally, in mathematics, one is
accustomed to regarding $a$ as either equal to $b$ or not.
However, this reflects a situation commonly encountered in geometry
when \emph{congruence} of geometric figures is considered.%
\index{congruence}
For example, in Euclidean space, two equilateral triangles of the same size are congruent in six (different)
ways.\footnote{Six, since we allow reflections, otherwise there are only three.\par
  \begin{tikzpicture}[tri/.style={draw,regular polygon,regular polygon sides=3,minimum height=6em}]
    \node[tri,rotate=-15]{};
    \begin{scope}[xshift=7em]
      \node[tri,rotate=15]{};
    \end{scope}
  \end{tikzpicture}
}
The chief novelty of univalent mathematics is that the basic logical notion of equality, as implemented by the identity types $a \eqto b$, is carefully
engineered to accommodate notions of congruence and symmetry from diverse areas of mathematics, including geometry.  Exposing that point of view
in the context of geometry is the main point of this book.

In light of the analogy with geometry just introduced,
we will refer to an element $i$ of $a \eqto a$ as a \emph{symmetry} of $a$.%
\index{symmetry!of an element}
Think, for example, of a congruence of a triangle with itself.
An example of a non-trivial symmetry will be seen in \cref{xca:C2}.

Consider the identity type $\fact(2) \eqto 2$, where $\fact$ denotes the factorial function defined in \cref{sec:natural-numbers}.
Expansion of the definitions in $\fact(2) \eqto 2$ simplifies it to $\Succ(\Succ(0)) \eqto \Succ(\Succ(0))$,
so we see from rule \ref{E2} that $\refl{\Succ(\Succ(0))}$ serves
as an element of it.\footnote{We will see later that numbers only have
trivial symmetries, so the possibility that there are other ways to
identify $\fact(2)$ with $2$ doesn't arise.}
We may also write either $\refl{2}$ or $\refl{\fact(2)}$ for that element.
A student might want a more detailed derivation that $\fact(2)$ may be identified with $2$,
but as a result of our convention above that definitions may be applied without changing anything, the application of definitions, including
inductive definitions, is normally regarded as a trivial operation, and the details are usually omitted.

We will refer to rule \ref{E3} as ``induction for identity''.
To signal that we wish to apply it, we may announce that we argue
\emph{by (path) induction on $e$}, or simply \emph{by path induction}.

The family $f$ resulting from an application of rule \ref{E3} may be regarded as having been completely defined by the single declaration
$f(a,\refl a) \defeq p$,
and indeed, we will often simply write such a declaration as a shorthand way of applying rule \ref{E3}.
The rule says that to construct something from every identification $e$ of $a$ with something else,
it suffices to consider the special case where the identification $e$ is $\refl a : a \eqto a$.%
\footnote{Notice that the single special case in such an induction corresponds to the single way of introducing elements of
identity types via rule \ref{E2}, and compare that with \ref{P4}, which dealt with the two ways of introducing elements of $\NN$.}

Intuitively, the induction principle for identity amounts to saying that the element $\refl a$ ``generates'' the system of types $a \eqto b$, as $b$
ranges over elements of $A$.\footnote{%
  We can also use a geometric intuition: when $b$ ``freely ranges'' over elements of $A$,
  together with a path $e : a \eqto b$,
  while we keep the element $a$ fixed, we can picture $e$ as a piece of string
  winding through $A$, and the ``freeness'' of the pair $(b,e)$ allows us to pull the string $e$,
  and $b$ with it, until we have the constant path at $a$, $\refl a$.\par
  \begin{tikzpicture}
    \draw plot [smooth cycle] coordinates {(0,0) (1.5,0) (1.3,1) (0,1.5)};
    \node[dot,label=above:$a$] (a) at (0.1,0.1) {};
    \node[dot,label=below:$b$] (b) at (1.3,0.8) {};
    \node (A1) at (1.5,1.5) {$A$};
    \draw[->] (a) .. controls ++(-20:1) and ++(170:1) .. node[auto] {$e$} (b);
    \node at (1.9,0.6) {$\mapsto$};
    \begin{scope}[xshift=2.5cm]
    \draw plot [smooth cycle] coordinates {(0,0) (1.5,0) (1.3,1) (0,1.5)};
    \node[dot,label=above:$a$] at (0.1,0.1) {};
    \node at (0.5,0.2) {$\refl a$};
    \node (A2) at (1.5,1.5) {$A$};
    \end{scope}
  \end{tikzpicture}
  Conversely, we can imagine $b$ starting at $a$ and $e$ starting out as $\refl a$, and then think of $b$ roaming throughout $A$, pulling
  the string $e$ along with it, until it finds every path from $a$ to some other element.
}

Equality relations are \emph{symmetric}. For identity types
we establish something similar, taking into account that
the notion of equality implemented here keeps track of the way
two things are identified, and there can be multiple ways.
Given a type $X$ and elements $a$ and $b$ of $X$,
we have an identity type $a \eqto b$
of (zero or more) identifications of $a$ with $b$. We also have
an identity type $b \eqto a$ of identifications of $b$ with $a$.
Symmetry now takes the form of a function from
type $a \eqto b$ to type $b \eqto a$, intuitively reversing
any identification of $a$ with $b$
to give an identification of $b$ with $a$.
In order to produce an element of $b \eqto a$ from an element $e$
of $a \eqto b$, for any $b$ and $e$, we argue by induction on $e$.
We let $P(b,e)$ be $b \eqto a$ for any $b$ of type $X$ and for
any $e$ of type $a \eqto b$, for use in rule \ref{E3} above.
Application of rule \ref{E3} reduces us to the case where $b$ is
$a$ and $p$ is $\refl a$, and our task is now to produce an
element of $a \eqto a$; we choose $\refl a$ for it.

Equality relations are also \emph{transitive}. We proceed in a
similar way as for symmetry. For each $a,b,c:X$ and for each
$p:a \eqto b$ and for each $q:b \eqto c$ we want to produce an
element of type $a \eqto c$.  By induction on $q$ we are reduced
to the case where $c$ is $b$ and $q$ is $\refl b$,
and we are to produce an element of $a \eqto b$.
The element $p$ serves the purpose.
%Notice the similarity of this inductive definition with the definition given above
%of the sum $m+n$. HMM ... (left versus right recursion)

Now we state our symmetry result a little more formally.

\begin{definition}\label{def:eq-symm}
  For any type $X$ and for any $a,b:X$, let
  $$\symm_{a,b} : (a \eqto b) \to (b \eqto a)$$
  be the function defined by induction by setting
  $\symm_{a,a}(\refl a) \defeq \refl a$.

  This operation on paths is called \emph{path inverse}, and we may abbreviate $\symm_{a,b}(p)$ as $p^{-1}$.
  \glossary(1-1){$p^{-1}$}{reverse identification, path inverse, \cref{def:eq-symm}}
\end{definition}

Similarly, we formulate transitivity a little more formally, as follows.

\begin{definition}\label{def:eq-trans}
  For any type $X$ and for any $a,b,c:X$, let $$\trans_{a,b,c} : (a \eqto b) \to ((b \eqto c) \to (a \eqto c))$$ be the function defined by induction by setting
  $(\trans_{a,b,b} (p)) (\refl b ) \defeq p$.

  This binary operation is called \emph{path composition} or \emph{path concatenation}\index{composition!of paths}\index{concatenation!of paths},
  and we may abbreviate $(\trans_{a,b,c}(p))(q)$ as either $p \ct q$, or as $q \cdot p$, $qp$, or $q \circ p$.
  \glossary(2conc){$p\protect\ct q, q\cdot p, qp, q\circ p$}{path concatenation or composition}
\end{definition}

The intuition that the path $p$ summarizes a gradual change from $a$ to $b$, and $q$ summarizes a gradual change from $b$ to $c$, leads to the
intuition that $p \ct q$ progresses gradually from $a$ to $c$ by first changing $a$ to $b$ and then changing $b$ to $c$; see
\cref{fig:path-concatenation}.

The notation $q\circ p$ for path composition, with $p$ and $q$ in reverse order,
fits our intution particularly well when the paths are related to functions and the composition of
the paths is related to the composition of the related functions in the same order, as happens, for example, in connection with {\em transport}
(defined below in \cref{def:transport}) in \cref{xca:trp-compose}.

\begin{marginfigure}
%  \centering
  \begin{tikzpicture}
    \node (X) at (0,-1.5) {$X$};
    \draw (0,-1)
    .. controls ++(200:-1) and ++(180:1) .. (2,-2)
    .. controls ++(180:-1) and ++(270:1) .. (4,0)
    .. controls ++(270:-1) and ++(20:2)   .. (2,2)
    .. controls ++(20:-2)   and ++(90:1)  .. (-1,0)
    .. controls ++(90:-1)  and ++(200:1) .. (0,-1);
    \node[dot,label=below:$a$] (a) at (0,0) {};
    \node[dot,label=below:$b$] (b) at (2,-1) {};
    \node[dot,label=above:$c$] (c) at (3,1) {};
    \node (ct) at (1.2,1) {$q\circ p \jdeq p\ct q$};
    \draw[->] (a) .. controls ++(-20:1) and ++(170:1) .. node[auto,swap] {$p$} (b);
    \draw[->] (b) .. controls ++(170:-1) and ++(-70:1) .. node[auto,swap] {$q$} (c);
    \draw[->] (a) .. controls ++(15:1) and ++(210:1) .. (c);
    %\draw (1,0) arc(210:330:.8 and .5);
    %\draw (2.09,-.18) arc(60:120:.8 and .7);
  \end{tikzpicture}
  \caption{Composition (also called concatenation) of paths in $X$}
  \label{fig:path-concatenation}
\end{marginfigure}

The types of $\symm_{a,b}$ and $\trans_{a,b,c}$ express that
$\eqto$ is symmetric and transitive. Another view of
$\symm_{a,b}$ and $\trans_{a,b,c}$ is that they are
operations on identifications, namely reversing an identification
and concatenating two identifications. The results of various
combinations of these operations can often be identified:
we formulate some of these identifications in the following exercise.

\begin{xca}\label{xca:path-groupoid-laws}
  Let $X$ be a type and let $a,b,c,d:X$ be elements.
  \begin{enumerate}
    \item For $p:a \eqto b$, construct an identification of type $p \ct \refl b \eqto p$.
    \item For $p:a \eqto b$, construct an identification of type $\refl a \ct p \eqto p$.
    \item For $p:a \eqto b$, $q:b \eqto c$, and $r:c \eqto d$, construct an identification of type $(p \ct q) \ct r \eqto p \ct (q \ct r)$.
    \item For $p:a \eqto b$, construct an identification of type $p^{-1} \ct p \eqto \refl b$.
    \item For $p:a \eqto b$, construct an identification of type $p \ct p^{-1} \eqto \refl a$.
    \item For $p:a \eqto b$, construct an identification of type $(p^{-1})^{-1} \eqto p$.
    \qedhere
  \end{enumerate}
\end{xca}

Given an element $p:a \eqto a$, we may use concatenation to define powers $p^n : a \eqto a$
by induction on $n:\NN$; we set $p^0\defeq\refl{a}$ and
$p^{n+1}\defeq p\cdot p^n$. Negative powers $p^{-n}$ are defined
as $(p^{-1})^n$.\footnote{We haven't yet assigned a meaning to $-n$,
  but after we introduce the set of integers $\zet$ below in~\cref{def:zet},
  we'll be justified in writing $p^z$ for any $z:\zet$.  See also \cref{exa:nnn}.}

One frequent use of elements of identity types is in \emph{substitution}\index{substitution}, which is
the logical principle that supports our intuition that when $x$ can by identified with $y$, we may replace $x$ by $y$
in mathematical expressions at will.  A wrinkle new to students will likely be that, in our logical framework
where there may be various ways to identify $x$ with $y$, one must specify the identification used in the substitution.
Thus one may prefer to speak of using an identification to \emph{transport} properties and data about $x$ to properties and data about $y$.

Here is a geometric example: if $x$ is a triangle of area $3$ in the plane, and $y$ is congruent to $x$, then $y$ also has area $3$.

Here is another example: if $x$ is a right triangle in the plane, and $y$ is congruent to $x$, then $y$ is also a right triangle, and
the congruence informs us which of the $3$ angles of $y$ is the right angle.

Now we introduce the notion more formally.

\begin{definition}\label{def:transport}
  Let $X$ be a type, and let $T(x)$ be a family of types parametrized by a variable $x:X$ (as discussed in \cref{univalent-mathematics}).
  Suppose $a,b:X$ and $e:a \eqto b$.
  Then we may construct a function of type $T(a) \to T(b)$.
  The function
  \[
  \trp[T]{e} : T(a) \to T(b)
  \]
  is defined by induction setting $\trp[T]{\refl{a}} \defeq \id_{T(a)}$.%
  \glossary(trp){$\protect\trp[T]{e}$}{transport function, \cref{def:transport}}
\end{definition}

The function thus defined may be called
\emph{the transport function in the type family $T$ along the path $e$},
or, less verbosely, \emph{transport}.\footnote{%
  We sometimes picture this schematically as follows:
  We draw $X$ as a (mostly horizontal) line,
  and we draw each type $T(x)$ as a vertical line lying over $x:X$.
  As $x$ moves around in $X$, these lines can change shape,
  and taken all together they form a $2$-dimensional blob lying over $X$.
  The transport functions map points between the vertical lines.\par
  \begin{tikzpicture}
    % Name the coordinates so they are easy to change
    % first: X
    \coordinate (X-left) at (-1,-1);
    \node[dot,label=below:$a$] (X-x) at (0,-1.2) {};
    \node[dot,label=below:$b$] (X-xp) at (1.5,-.9) {};
    \coordinate (X-right) at (2.8,-1);
    \node (X) at (3,-1) {$X$};
    % then: T top and bottom
    \coordinate (T-top-left) at (-1,1.5);
    \coordinate (T-bot-left) at (-1,0.5);
    \coordinate[label=above:$T(a)$] (T-top-x) at (0,1.9);
    \coordinate (T-bot-x) at (0,-.1);
    \coordinate[label=above:$T(b)$] (T-top-xp) at (1.5,2.1);
    \coordinate (T-bot-xp) at (1.5,.2);
    \coordinate (T-top-right) at (2.8,1.3);
    \coordinate (T-bot-right) at (2.8,0.8);
    \draw (T-bot-left) .. controls +(-90:.5) and +(0:-.5) .. (T-bot-x)
    .. controls +(0:.5) and +(-10:-.5) .. (T-bot-xp)
    .. controls +(-10:.5) and +(90:-.5) .. (T-bot-right)
    -- (T-top-right)
    .. controls +(90:.5) and +(0:.5) .. (T-top-xp)
    .. controls +(0:-.5) and +(-10:.4) .. (T-top-x)
    .. controls +(-10:-.4) and +(90:.5) .. (T-top-left)
    -- (T-bot-left);
    \draw[dashed] (T-bot-x) -- (T-top-x);
    \draw[dashed] (T-bot-xp) -- (T-top-xp);
    \draw (X-left) .. controls +(-10:.3) and +(0:-.3) .. (X-x);
    \draw[->] (X-x) .. controls +(0:.3) and +(-10:-.5) ..
      node[anchor=north] {$e$} (X-xp);
    \draw (X-xp) .. controls +(-10:.5) and +(0:-.1) .. (X-right);
    % Now the specifics: a point t and its transport to T(x')
    \node[dot,label=left:$t$] (t) at (0,0.9) {};
    \node[dot,label=right:${\trp[T]e(t)}$] (tp) at (1.5,1.1) {};
    \draw[mapsto] (t) .. controls +(0:.5) and +(0:-.5) .. (tp);
  \end{tikzpicture}}%
\index{transport}
We may also simplify the notation to just $\trp e$.
The transport functions behave as expected: we may construct an identification of type $\trp {e'\circ e} \eqto \trp {e'} \circ \trp {e}$.
In words: transport along the composition $e\circ e'$ can be identified with the composition of the two
transport functions.  This may be proved by induction in the following exercise.

\begin{xca}\label{xca:trp-compose}
  Let $X$ be a type, and let $T(x)$ be a family of types parametrized by a variable $x:X$.
  Suppose we are given elements $a,b,c:X$, $e:a \eqto b$, and $e':b \eqto c$.  Construct an identification of type
  \[
    \trp {e'\circ e} \eqto \trp {e'} \circ \trp {e}.\qedhere
  \]
\end{xca}

Yet another example of good behavior is given in the following exercise.

\begin{xca}\label{xca:trp-nondep}
  Let $X,Y$ be types.
  As discussed in \cref{univalent-mathematics}, we may regard the expression $Y$ as a constant family of types parametrized by a variable $x:X$.
  Produce an identification of type $\trp[Y]{p} \eqto \id_Y$, for any path $p:a \eqto b$.
\end{xca}

In \cref{sec:props-sets-grpds} below we will discuss what it means for a type to have at most one element.
When the types $T(x)$ may have more than one element,
we may regard an element of $T(x)$ as providing additional \emph{structure} on $x$.
In that case, we will refer to the transport function $\trp e : T(a) \to T(b)$ as
\emph{transport of structure} from $a$ to $b$.

Take, for example, $T(x)\defeq (x \eqto x)$.
Then $\trp e$ is of type $(a \eqto a) \to (b \eqto b)$ and transports a
symmetry of $a$ to a symmetry of $b$.

By contrast, when the types
$T(x)$ have at most one element, we may regard an element of $T(x)$
as providing a proof of a property of $x$. In that case, the transport
function $\trp e : T(a) \to T(b)$ provides a way to establish a claim about $b$
from a claim about $a$, so we will refer to it as \emph{substitution}.  In
other words, elements that can be identified have the same properties.

\section{Product types}
\label{sec:product-types}

Functions and product types have been introduced in \cref{univalent-mathematics}, where we have also explained how to create a function by
enclosing a family of elements in one.  In this section we treat functions and product types in more detail.

Recall that if $X$ is a type and $Y(x)$ is a family of types parametrized by a variable $x$ of type $X$, then there is a \emph{product type}\footnote{%
  Also known as a \emph{Pi-type}.}
$\prod_{x:X} Y(x)$ whose elements $f$ are functions that provide elements $f(a)$ of type $Y(a)$, one for each $a:X$.  We will refer to $X$ as the
\emph{parameter type} of the product.%
\index{product type}\index{Pi type}\index{parameter type}
By contrast, if $Y$ happens to be a constant family of types, then
$\prod_{x:X} Y$ will also be denoted by $X \to Y$, and it will also be called a \emph{function type}.

If $X$ and $Y(x)$ are elements of a universe $\UU$, then so is $\prod_{x:X} Y(x)$.

Functions preserve identity, and we will use this frequently later on.  More precisely, functions induce maps on identity types, as the
following definition makes precise.

\begin{definition}\label{def:ap}
For all types $X$, $Y$, functions $f:X\to Y$ and elements $x,x':X$, the function
$$\ap{f,x,x'} : (x \eqto x') \to (f(x) \eqto f(x'))$$ is defined by induction by setting
$\ap{f,x,x}(\refl{x})\defeq\refl{f(x)}$.%
\glossary(ap){$\protect\ap{f}$}{application of $f$ to a path, \cref{def:ap}}
\glossary(ap){$f(p)$}{application of $f$ to the path $p$, \cref{def:ap}}
\end{definition}

The function $\ap{f,x,x'}$, for any elements $x$ and $x'$ of $X$, is called an \emph{application} of $f$ to paths or to identifications,
and this explains the choice of the symbol $\ap{}$ in the notation for it.
It may also be called the function (or map) \emph{induced} by $f$ on identity types.

When $x$ and $x'$ are clear from the context, we may abbreviate $\ap{f,x,x'}$ by writing $\ap{f}$ instead.
For convenience, we may abbreviate it even further, writing $f(p)$ for $\ap f (p)$.

The following lemma shows that $\ap f$ is compatible with composition.

\begin{construction}\label{lem:apcomp}
  Given a function $f:X\to Y$, and elements $x,x',x'':X$, and paths $p : x \eqto x'$ and $p' : x' \eqto x''$,
  we have an identification of type $\ap f (p' \cdot p) \eqto  \ap f (p') \cdot  \ap f (p)$.

  Similarly, we have that $\ap f$ is compatible with path inverse
  in that we have an identification of type
  $\ap f(p^{-1}) \eqto  (\ap f (p))^{-1}$ for all $p : x \eqto x'$.

  Finally, we have an identification of type $\ap \id (p) \eqto p$ for all
  $p : x \eqto x'$.
\end{construction}

\begin{implementation}{lem:apcomp}
  By induction on $p$ and $p'$, one reduces to producing an identification of type
  \[
    \ap f (\refl x \cdot \refl x) \eqto  \ap f ( \refl x ) \cdot  \ap f ( \refl x ).
  \]
  Both $\ap f (\refl x \cdot \refl x)$ and
  $\ap f ( \refl x ) \cdot  \ap f ( \refl x )$
  are equal to $\refl { f(x) }$ by definition,
  so the identification $\refl {\refl { f(x) }}$ has the desired type.

  The other two parts of the construction are also easily done by induction on $p$.
\end{implementation}

\begin{xca}\label{xca:trp-ap}
  Let $X$ be a type and $T(x)$ a family of types parametrized by a variable $x:X$. Furthermore, let $A$ be a type, let $f:A\to X$ be a
  function, let $a$ and $a'$ be elements of $A$, and let $p: a \eqto a'$ be a path.
  Verify that the two functions $\trp[T \circ f]{p}$ and $\trp[T]{\ap{f}(p)}$ are of type $T(f(a)) \to T(f(a'))$.
  Then construct an identification between them, i.e., construct an element of type $\trp[T \circ f]{p} \eqto \trp[T]{\ap{f}(p)}$.
\end{xca}

If two functions $f$ and $g$ of type $\prod_{x:X} Y(x)$ can be identified, then their values can be identified, i.e., for every element $x$ of
$X$, we may produce an identification of type $f(x) \eqto g(x)$, which can be constructed by induction, as follows.

\begin{definition}\label{def:ptw}
  Let $f,g:\prod_{x:X} Y(x)$. Define the function
  \[
    {\ptw}_{f,g}: ( f \eqto g ) \to \left( \prod_{x:X} f(x) \eqto g(x) \right),
  \]
  by induction by setting ${\ptw}_{f,f}(\refl{f}) \defeq x \mapsto \refl{f(x)}$.
  \footnote{The notation $\ptw$ is chosen to remind the reader of the word ``point-wise'', because the identifications are provided just for each
  point $x$.   An alternative approach goes by considering, for any $x:X$, the evaluation function $\ev_x : \big(\prod_{x:X} Y(x)\bigr) \to Y(x)$ defined by
    $\ev_x(f) \defeq f(x)$.  Then one could define ${\ptw}_{f,g}(p,x) \defeq \ap{\ev_x}(p)$.  The functions provided by these two definitions
  are not equal by definition, but they can be identified, and one can easily be used in place of the other.}
\end{definition}

Conversely, given $f,g:\prod_{x:X} Y(x)$,
from a basic axiom called \emph{function extensionality},%
\index{function extensionality}
postulated below in \cref{def:funext}, an identification $f \eqto g$
can be produced from a family of identifications of type $f(x) \eqto g(x)$
parametrized by a variable $x$ of type $X$.

\begin{definition}\label{def:naturality-square}
Let $X,Y$ be types and $f,g: X\to Y$ functions.
Given an element $h$ of type $\prod_{x:X} f(x) \eqto g(x)$, elements $x$ and $x'$ of $X$, and a path $p: x \eqto x'$,
we have two elements $h(x')\cdot \ap{f}(p)$ and $\ap{g}(p)\cdot h(x)$ of type $f(x) \eqto g(x')$.
We construct an identification
\[
  \ns(h,p): \left(h(x')\cdot \ap{f}(p) \eqto \ap{g}(p)\cdot h(x)\right),
\]
between them by induction, by setting $\ns(h,\refl{x})$ to be some
element of $h(x) \cdot \refl{f(x)} \eqto h(x)$, which can be constructed by induction, as in Exercise \ref{xca:path-groupoid-laws}.%
\glossary(ns){$\protect\ns$}{naturality square, \cref{def:naturality-square}}
The type of $\ns(h,p)$ can be depicted as a square\footnote{%
  \begin{displaymath}
    \begin{tikzcd}[column sep=large,row sep=large,ampersand replacement=\&]
      f(x) \ar[r,"="',"\ap f(p)"] \ar[d,"=","h(x)"'] \& f(x') \ar[d,"="',"h(x')"] \\
      g(x) \ar[r,"=","\ap g(p)"']                    \& g(x')
    \end{tikzcd}
  \end{displaymath}%
} and $\ns(h,p)$ is called a \emph{naturality square}.%
\index{naturality square}
%\footnote{This terminology comes from category theory.}
\end{definition}

\section{Identifying elements in members of families of types}

If $Y(x)$ is a family of types parametrized by a variable $x$ of type $X$, and $a$ and $a'$ are elements of type $X$, then after identifying $a$
with $a'$ it turns out that it is possible to ``identify'' an element of $Y(a)$ with an element of $Y(a')$, in a certain sense.  That is the
idea of the following definition.

\begin{definition}\label{def:pathsoverpaths}
  Suppose we are given a type $X$ in a universe $\UU$ and a family of 
  types $Y(x)$, also in $\UU$, parametrized by a variable $x$ of type $X$.
  Given elements $a,a':X$, $y:Y(a)$, and
  $y':Y(a')$ and a path $p : a \eqto a'$,
  we define a new type $\pathover y Y p {y'}$ in $\UU$ as follows.%
  \glossary(2=over){$\protect\pathover y Y p {y'}$}{path-over type,
    \cref{def:pathsoverpaths}}
  We proceed by induction on $a'$ and $p$, which reduces us to the case where $a'$ is $a$ and $p$ is $\refl a$,
  rendering $y$ and $y'$ of the same type $Y(a)$ in $\UU$, allowing us to define
  $\pathover y Y {\refl a} {y'}$ to be $y \eqto y'$, which is also in $\UU$.
\end{definition}

An element $q : \pathover y Y p {y'}$ is called an \emph{identification} of $y$ with $y'$ \emph{over} $p$, or a
\emph{path} from $y$ to $y'$ \emph{over} $p$.\index{path over}
Intuitively, we regard $p$ as specifying a way for $a$ to change gradually into $a'$, and this provides a way
for $Y(a)$ to change gradually into $Y(a')$; then $q$ charts a way for $y$ to change gradually into $y'$ as $Y(a)$ changes gradually into $Y(a')$.\footnote{\label{ft:path-over-pic}%
  We picture this as follows: the path from $y$ to $y'$ over $p$ travels
  through the vertical lines representing the types $Y(x)$ as $x:X$
  moves along the path $p$ in $X$ from $a$ to $a'$:\par
\begin{tikzpicture}
  % Name the coordinates so they are easy to change
  % first: X
  \coordinate (X-left) at (-1,-1);
  \node[dot,label=below:$a$] (X-x) at (0,-1.2) {};
  \node[dot,label=below:$a'$] (X-xp) at (1.5,-.9) {};
  \coordinate (X-right) at (2.8,-1);
  \node (X) at (3,-1) {$X$};
  % then: Y top and bottom
  \coordinate (Y-top-left) at (-1,1.5);
  \coordinate (Y-bot-left) at (-1,0.5);
  \coordinate[label=above:$Y(a)$] (Y-top-x) at (0,1.9);
  \coordinate (Y-bot-x) at (0,-.1);
  \coordinate[label=above:$Y(a')$] (Y-top-xp) at (1.5,2.1);
  \coordinate (Y-bot-xp) at (1.5,.2);
  \coordinate (Y-top-right) at (2.8,1.3);
  \coordinate (Y-bot-right) at (2.8,0.8);
  \draw (Y-bot-left) .. controls +(-90:.5) and +(0:-.5) .. (Y-bot-x)
  .. controls +(0:.5) and +(-10:-.5) .. (Y-bot-xp)
  .. controls +(-10:.5) and +(90:-.5) .. (Y-bot-right)
  -- (Y-top-right)
  .. controls +(90:.5) and +(0:.5) .. (Y-top-xp)
  .. controls +(0:-.5) and +(-10:.4) .. (Y-top-x)
  .. controls +(-10:-.4) and +(90:.5) .. (Y-top-left)
  -- (Y-bot-left);
  \draw[dashed] (Y-bot-x) -- (Y-top-x);
  \draw[dashed] (Y-bot-xp) -- (Y-top-xp);
  \draw (X-left) .. controls +(-10:.3) and +(0:-.3) .. (X-x);
  \draw[->] (X-x) .. controls +(0:.3) and +(-10:-.5) ..
    node[anchor=north] {$p$} (X-xp);
  \draw (X-xp) .. controls +(-10:.5) and +(0:-.1) .. (X-right);
  % Now the specifics: two points y,y' and the pathover
  \node[dot,label=left:$y$] (y) at (0,0.9) {};
  \node[dot,label=right:$y'$] (yp) at (1.5,1.1) {};
  \draw[->] (y) .. controls +(0:.5) and +(0:-.5) ..
    node[anchor=south] {$q$} (yp);
  \end{tikzpicture}}%

\begin{remark} 
Given a type $Z$, \cref{def:pathsoverpaths} has a special case
in which $Y(x)\defeq Z$ for all $x:X$.
Given elements $a,a':X$, a path $p : a \eqto a'$ and elements $z,z':Z$, 
we can form both the type $\pathover z Y p {z'}$ and the identity 
type $z\eqto z'$. These types are readily identified by induction on $p$.
\end{remark}


The following definition identifies the type of paths over $p$ with a type
of paths using transport along $p$.

\begin{definition}\label{def:pathover-trp}
In the context of \cref{def:pathsoverpaths}, define by induction on $p$ an
identification
$\po_p: \left(\pathover y Y p {y'}\right) \eqto \left( \trp[Y]{p}(y) \eqto y'\right)$ in $\UU$,
by setting $\po_{\refl{x}} \defeq \refl{y \eqto y'}$.%
\glossary(po){$\protect\po_p$}{convert path over path, \cref{def:pathover-trp}}
\end{definition}

Many of the operations on paths have counterparts for paths over paths.
For example, we may define composition of paths over paths as follows.

\begin{definition}\label{def:pathovercomposition}
  Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
  Suppose also that we have elements $x, x', x'' : X$, a path $p : x \eqto x'$, and a path $p' : x' \eqto x''$.
  Suppose further that we have elements $y : Y(x)$, $y' : Y(x')$, and $y'' : Y(x'')$, with paths $q : \pathover y Y p {y'}$ over $p$
  and $q' : \pathover {y'} Y {p'} {y''}$ over $p'$.
  Then we define the \emph{composite} path $(q' \pathovercomp q) : \pathover y Y {p' \circ p} {y''}$ over $p' \circ p$ as follows.
  First we apply path induction on $p'$ to reduce to the case where $x''$ is $x'$ and $p'$ is $\refl{x'}$.
  That also reduces the type $\pathover {y'} Y {p'} {y''}$ to the identity type $y' \eqto y''$, so we may apply path induction on $q'$ to reduce
  to the case where $y''$ is $y'$ and $q'$ is $\refl{y'}$.
  Now observe that $p' \circ p$ is $p$, so $q$ provides the element we need.
\end{definition}

Similarly, one can define the inverse of a path over a path,
writing $\inv q : \pathover {y'} Y {\inv p} y$ for the inverse
of $q : \pathover y Y p {y'}$.
For these operations on paths over paths we have identifications
analogous to those for the operations on paths in
\cref{xca:path-groupoid-laws}, after some modification.
For example,
${\inv g} \pathovercomp q$ of type $\pathover {y} Y {{\inv p}\circ p} y$ and
$\refl{y}$ of type $\pathover {y} Y {\refl{x}} y$ cannot be directly used
to form an identity type, since their types are not equal by definition.
We will state these identifications when we need them.

\begin{xca}\label{xca:cp}
Try to state some of these identifications yourself.
\end{xca}

The following construction shows how to handle application of a dependent
function $f$ to paths using the definition above.

\begin{definition}\label{def:apd}
  Suppose we are given a type $X$, a family of types $Y(x)$ parametrized by the elements $x$ of $X$, and a function $f:\prod_x Y(x)$.
  Given elements $x,x':X$ and a path $p : x \eqto x'$, we define
  \[
    \apd{f}(p) : \pathover {f(x)} Y p {f(x')}
  \]
  by induction on $p$, setting
  \[
    \apd f {(\refl x)} \defeq \refl {f(x)}.\qedhere
    \]
    \glossary(apd){$\protect \apd f$}{application of a dependent function
    to a path, \cref{def:apd}}
    \glossary(apd){$f(p)$}{application of dependent $f$ to the path $p$ \cref{def:apd}}
\end{definition}

The function $\apd f$ is called \emph{dependent application} of $f$ to paths.\footnote{%
  We picture $f$ via its \emph{graph} of the values $f(x)$
  as $x$ varies in $X$.
  The dependent application of $f$ to $p$ is then the piece of the graph
  that lies over $p$:\par
  \begin{tikzpicture}
    % Name the coordinates so they are easy to change
    % first: X
    \coordinate (X-left) at (-1,-1);
    \node[dot,label=below:$x$] (X-x) at (0,-1.2) {};
    \node[dot,label=below:$x'$] (X-xp) at (1.5,-.9) {};
    \coordinate (X-right) at (2.8,-1);
    \node (X) at (3,-1) {$X$};
    % then: Y top and bottom
    \coordinate (Y-top-left) at (-1,1.5);
    \coordinate (Y-bot-left) at (-1,0.5);
    \coordinate[label=above:$Y(x)$] (Y-top-x) at (0,1.9);
    \coordinate (Y-bot-x) at (0,-.1);
    \coordinate[label=above:$Y(x')$] (Y-top-xp) at (1.5,2.1);
    \coordinate (Y-bot-xp) at (1.5,.2);
    \coordinate (Y-top-right) at (2.8,1.3);
    \coordinate (Y-bot-right) at (2.8,0.8);
    \draw (Y-bot-left) .. controls +(-90:.5) and +(0:-.5) .. (Y-bot-x)
    .. controls +(0:.5) and +(-10:-.5) .. (Y-bot-xp)
    .. controls +(-10:.5) and +(90:-.5) .. (Y-bot-right)
    -- (Y-top-right)
    .. controls +(90:.5) and +(0:.5) .. (Y-top-xp)
    .. controls +(0:-.5) and +(-10:.4) .. (Y-top-x)
    .. controls +(-10:-.4) and +(90:.5) .. (Y-top-left)
    -- (Y-bot-left);
    \draw[dashed] (Y-bot-x) -- (Y-top-x);
    \draw[dashed] (Y-bot-xp) -- (Y-top-xp);
    \draw (X-left) .. controls +(-10:.3) and +(0:-.3) .. (X-x);
    \draw[->] (X-x) .. controls +(0:.3) and +(-10:-.5) ..
      node[anchor=north] {$p$} (X-xp);
    \draw (X-xp) .. controls +(-10:.5) and +(0:-.1) .. (X-right);
    % Now the specifics: two points y,y' and the pathover
    \coordinate (y-left) at (-1,1.2);
    \node[dot,label=below left:$f(x)$] (y) at (0,0.9) {};
    \node[dot,label=below right:$f(x')$] (yp) at (1.5,1.1) {};
    \coordinate (y-right) at (2.8,1);
    \draw[dotted] (y-left) .. controls +(-10:.3) and +(0:-.5) .. (y);
    \draw[->] (y) .. controls +(0:.5) and +(0:-.5) ..
      node[anchor=south] {$\apd f(p)$} (yp);
    \draw[dotted] (yp) .. controls +(0:.5) and +(120:.1) .. (y-right);
  \end{tikzpicture}}
For convenience, we may abbreviate $\apd f (p)$ to $f(p)$,
when there is no risk of confusion.

The following construction shows how functions of two variables may be applied to paths over paths.

\begin{definition}\label{def:applfun2}
  Suppose we are given a type $X$, a family of types $Y(x)$ parametrized by the elements $x$ of $X$, and a type $Z$.
  Suppose also we are given a function $g : \prod_{x:X} (Y(x) \to Z)$ of two variables.
  Given elements $x,x':X$, $y:Y(x)$, and
  $y':Y(x')$, a path $p : x \eqto x'$, and a path $q :\pathover y Y p {y'}$ over $p$,
  we may construct a path
  \[
    \apap g p q : g(x)(y) \eqto g(x')(y')
  \]
  by induction on $p$ and $q$, setting
  \[
    \apap g {\refl x}{\refl y} \defeq \refl {g(x)(y)}.\qedhere
  \]
\end{definition}

The function $p \mapsto q \mapsto \apap g p q$ is called \emph{application} of $g$ to paths over paths.
For convenience, we may abbreviate $\apap g p q$ to $g(p)(q)$.

The following definition will be useful later.

\begin{definition}\label{def:applfun2comp}
  Suppose we are given a type $X$, a family of types $Y(x)$ parametrized by the elements $x$ of $X$, and a type $Z$.  Suppose also we are given
  a function $g : \prod_{x:X} (Y(x) \to Z)$ of two variables.  Given an element $x:X$, elements $y, y':Y(x)$, and an identification $q : y \eqto y'$, then
  we define an identification of type $\apap g {\refl x} q \eqto \ap {g(x)}(q)$, by induction on $q$, thereby reducing to the case where $y'$ is
  $y$ and $q$ is $\refl y$, rendering the two sides of the equation equal, by definition, to $\refl {g(x)(y)}$.
\end{definition}

\section{Sum types}
\label{sec:sum-types}

There are \emph{sums} of types.
By this we mean if $X$ is a type and $Y(x)$ is a family of types parametrized by a variable $x$ of type $X$, then
there will be a type\footnote{%
  Also known as a \emph{Sigma-type}.}
$\sum _{x:X} Y(x)$%
\index{type!sum}\index{sum type}\index{type!Sigma}\index{sigma type}%
\glossary(918Sigma1){$\sumop _{x:X} Y(x)$}{sum type, of dependent pairs $(x,y)$}
whose elements are all pairs $(a,b)$, where $a:X$ and $b:Y(a)$. Since the type of $b$ may depend on $a$ we also call such a pair
a \emph{dependent} pair. We may refer to $X$ as the \emph{parameter
  type} of the sum.\footnote{%
  We may denote $\sum_{x:X}Y(x)$ by $\Tot(Y)$
  and also call it the \emph{total type} of the family $Y(x)$.
  \index{total type}
  \glossary(totaltype){$\protect\Tot(Y)$}{the total type $\protect\sum_{x:X}Y(x)$}
  We can picture it, in the style of the pictures above,
  as the entire blob lying over $X$. (Each $Y(x)$ is a vertical line over $x:X$,
  and a point $y:Y(x)$ becomes a point $(x,y)$ in the blob.)\par
  \begin{tikzpicture}
    % Name the coordinates so they are easy to change
    % first: X
    \coordinate (X-left) at (-1,-1);
    \node[dot,label=below:$x$] (X-x) at (1,-1.2) {};
    \coordinate (X-right) at (2.8,-1);
    \node (X) at (3,-1) {$X$};
    \node (SXY) at (3,2) {${\sum_{x:X}Y(x)}$};
    % then: Y top and bottom
    \coordinate (Y-top-left) at (-1,1.5);
    \coordinate (Y-bot-left) at (-1,0.5);
    \coordinate[label=above:$Y(x)$] (Y-top-x) at (1,1.9);
    \coordinate (Y-bot-x) at (1,-.1);
    \coordinate (Y-top-right) at (2.8,1.3);
    \coordinate (Y-bot-right) at (2.8,0.8);
    \draw (Y-bot-left) .. controls +(-90:.5) and +(0:-.5) .. (Y-bot-x)
    .. controls +(0:.5) and +(90:-.5) .. (Y-bot-right)
    -- (Y-top-right)
    .. controls +(90:.5) and +(-10:.4) .. (Y-top-x)
    .. controls +(-10:-.4) and +(90:.5) .. (Y-top-left)
    -- (Y-bot-left);
    \draw[dotted] (Y-bot-x) -- (Y-top-x);
    \draw (X-left) .. controls +(10:.3) and +(0:-.3) .. (X-x);
    \draw (X-x) .. controls +(0:.3) and +(0:-.1) .. (X-right);
    % Now the specifics: the pair (x,y) and the projection
    \node[dot,label=left:${(x,y)}$] (y) at (1,0.9) {};
    \draw[->,shorten <=.1cm,shorten >=.1cm] (Y-bot-x)
    -- node[anchor=west] {${\fst}$} (X-x);
  \end{tikzpicture}}

If $X$ and $Y(x)$ are elements of a universe $\UU$, then so is $\sum _{x:X} Y(x)$.

Proving something about (or constructing something from) every
element of $\sum _{x:X} Y(x)$ is done by performing the construction on elements of the form $(a,b)$, for every $a:X$ and $b: Y(a)$.
Two important examples of such constructions are:
\begin{enumerate}
\item \emph{first projection},
$\fst:(\sum _{x:X} Y(x)) \to X$,
$\fst(a,b)\defeq a$;
\item\label{it:second-projection} \emph{second projection},
$\snd(a,b): Y(a)$,
$\snd(a,b)\defeq b$.
\end{enumerate}
In \ref{it:second-projection}, the type of $\snd$ is, in full,
$\prod_{z:\sum_{x:X} Y(x)} Y(\fst(z))$.

\begin{remark}
  \label{rem:non-dependent-sums}
  An important special case of sum types is when the type $Y(x)$ does
  not depend on $x:X$. In that case the sum type $\sum _{x:X} Y(x)$
  is denoted as $X\times Y$ and called a \emph{binary product type},
  see \cref{sec:binprod-types}.
\end{remark}

\begin{remark}
  \label{rem:iterated-sums}
  One may consider sums of sums.  For example, suppose $X$ is a type, suppose $Y(x)$ is a family of types parametrized by a variable $x$ of type $X$,
  and suppose $Z(x,y)$ is a family of types parametrized by variables $x:X$ and $y:Y(x)$.  In this case, the \emph{iterated sum}
  $\sum_{x:X} \sum_{y:Y(x)} Z(x,y)$ consists of pairs of the form $(x,(y,z))$.  For simplicity, we introduce the notation
  $(x,y,z) \defeq (x,(y,z))$, and refer to $(x,y,z)$ as a \emph{triple} or as a \emph{$3$-tuple}.\index{triple}
  \marginnote{%
  Another example of an iterated sum is when $Z'(u)$ is a family of types
  parameterized by a variable $u$ of type $\sum_{x:X} Y(x)$.
  Elements of the type $\sum_{u:\sum_{x:X} Y(x)}Z'(u)$ are triples
  $((x,y),z)$. We use the triple-notation also for this case.}

That process can be repeated: suppose $X_1$ is a type, suppose $X_2(x_1)$
is a family of types parametrized by a variable $x_1$ of type $X_1$,
suppose $X_3(x_1,x_2)$ is a family of types parametrized by variables
$x_1:X_1$ and $x_2:X_2(x_1)$, and so on, up to a family
  $X_n(x_1,\dots,x_{n-1})$ of types.  In this case, the \emph{iterated sum}
  $$\sum _{x_1:X_1} \sum_{x_2:X_2(x_1)} \dots \sum_{x_{n-1}:X_{n-1}(x_1,\dots,x_{n-2})} X_n(x_1,\dots,x_{n-1}) $$
  consists of elements of the form
  $(x_1,(x_2,(\dots (x_{n-1},x_n)\dots)))$; each such element is a pair whose second member is a pair, and so on, so we may refer to it as an \emph{iterated pair}.
  For simplicity, we introduce the notation $(x_1,x_2,\dots,x_n)$ for such an iterated pair, and refer to it as an \emph{$n$-tuple}.\index{tuple}
\end{remark}

\section{Equivalences}\label{sec:equivalence}

Using a combination of sum, product, and identity types allows
us to express important notions, as done in the following
definitions.

The property that a type $X$ has ``exactly one element'' may be made precise
by saying that $X$ has an element such that every other element is equal to it.
This property is encoded in the following definition.

\begin{definition}
  \label{def:contractible}
  Given a type $X$, define a type $\iscontr(X)$ by setting
  \[
    \iscontr(X) \defeq \sum_{c:X} \prod_{x:X} (c \eqto x).\qedhere
  \]
\end{definition}

If $ (c,h) : \iscontr(X) $, then $c$ will be called the \emph{center} of the
the \emph{contraction} $h$, and we call the type $X$ \emph{contractible}.

By path composition, one sees that any element $x : X$ can serve as the center of a contraction of a contractible type $X$.

The following lemma gives an important example of a contractible type.

Given a type $X$ and an element $a$ of $X$,
the \emph{singleton type} $\sum_{x:X} (a \eqto x)$
consists of pairs $(x,i)$ with $i: a \eqto x$. The following lemma shows that a singleton type has exactly one element, justifying the name.

\begin{lemma}\label{lem:thepathspaceiscontractible}
For any type $X$ and $a:X$, the singleton type $\sum_{x:X} (a \eqto x)$ is contractible.
\end{lemma}

\begin{proof}
Take as center the pair $(a,\refl{a})$. We have
to produce, for any element $x$ of $X$ and for any identification
$i: a \eqto x$, an identification of type $(a,\refl{a}) \eqto (x,i)$.  This is done by path induction on $i$, which reduces us to producing
an identification of type $(a,\refl{a}) \eqto (a,\refl{a})$; reflexivity provides one, namely $\refl{(a,\refl{a})}$.
\end{proof}

\begin{definition}
\label{def:fiber}
Given a function $f : X \to Y$ and an element $y:Y$,
the \emph{fiber} (or \emph{preimage}) $f^{-1}(y)$
\index{fiber}\index{preimage}
is encoded by defining $$f^{-1}(y) \defeq \sum_{x:X}(y \eqto f(x)).$$
In other words, an element of the fiber $f^{-1}(y)$ is a pair consisting
of an element $x$ of $X$ and an identification of type $y \eqto f(x)$.
\end{definition}

In set theory, a function $f : X \to Y$ is a bijection if and only if
all preimages $f^{-1}(y)$ consist of exactly one element.
We can also express this in type theory, in a definition due
to Voevodsky, for types in general.

\begin{definition}
  \label{def:equivalence}
  A function $f : X \to Y$ is called an \emph{equivalence} if $\inv f(y)$ is contractible for
  all $y:Y$.  The condition is encoded by the type
\[
\isEq(f) \defeq \prod_{y:Y}\iscontr(f^{-1}(y)).\qedhere
\]
\end{definition}

We may say that $X$ and $Y$ are \emph{equivalent} if we
have an equivalence between them.

\begin{definition}
  \label{def:type-of-equivalences}
  We define the type $X \equivto Y$ of equivalences from $X$ to $Y$
  by the following definition.%
  \glossary(2equivto){$\protect\equivto$}{type of equivalences}
  \[
  (X \equivto Y) \defeq \sum_{f:X\to Y} \isEq(f).\qedhere
  \]
\end{definition}

Suppose $f:X \equivto Y$ is an equivalence, and let $t(y): \iscontr(f^{-1}(y))$, for each $y:Y$, be the corresponding witness to contractibility of the fiber.
Using $t$ we can define an inverse function $g : Y \to X$ by setting $g(y)\defeq\fst(\fst(t(y)))$. This can be seen as follows.

By unfolding all the definitions\footnote{%
  Note that $\fst(t(y)) : \inv f(y)$, so $\fst(\fst(t(y))) : X$ with
  $\snd(\fst(t(y))) : y \eqto f(\fst(\fst(t(y)))).$},
  we have an identification of type $f(g(y)) \eqto y$.
Moreover, $(x,\refl{f(x)})$ is an element of the
fiber $f^{-1}(f(x))$, and $t(f(x))$ is a proof
that this fiber is contractible. Hence the center of contraction
$\fst(t(f(x))$ is identified with $(x,\refl{f(x)})$, and so
$g(f(x))\jdeq(\fst(\fst(t(f(x))))) \eqto x$.

We have shown that $f$ and $g$ are inverse functions.
When it won't cause confusion with the notation for the fibers of $f$,
we will write $f^{-1}$ instead of $g$.

For any type $X$, the identity function $\id_X$ is an
equivalence from $X$ to $X$. To see that, observe that for every
element $a$ in $X$,
$\id_X^{-1}(a)$ is a singleton type and hence is contractible.
This observation, combined with the fact that
$\trp[T]{\refl{x}}\jdeq \id_{T(x)}$, gives that
the function $\trp[T]{e}$ from \cref{def:transport}
is an equivalence from $T(x)$ to $T(y)$, for all $e: x \eqto y$.

\begin{xca}\label{xca:equivalence-invers}
Make sure you understand the two applications of $\fst$
in the definition $f^{-1}(y)\defeq\fst(\fst(t(y)))$ above.
Show that $f^{-1}$ is an equivalence from $Y$ to $X$.
Give a function $(X\equivto Y) \to (Y\equivto X)$.
% and show that our function is an equivalence. Too difficult here.
\end{xca}

\begin{xca}\label{xca:equivalence-comp}
Give  a function $(X\equivto Y) \to ((Y\equivto Z) \to (X\equivto Z))$.
\end{xca}

\begin{xca}\label{xca:2-out-of-3}
  Consider types $A$, $B$, and $C$, functions $f:A\to B$, $g:A\to C$ and $h:B\to C$, together with an element $e: hf \eqto g$.  Prove that if two of
  the three functions are equivalences, then so is the third one.
\end{xca}

The following lemma gives an equivalent characterization
of equivalence that is sometimes easy to use.

\begin{construction}\label{lem:weq-iso}
  Let $X,Y$ be types. For each equivalence $f: X\to Y$, we have a function $g: Y\to X$ such that for all $x:X$ we have $g(f(x)) \eqto x$ and for all
  $y:Y$ we have $f(g(y)) \eqto y$. Conversely, if we have such a function $g$, then $f$ is an equivalence.
\end{construction}
\begin{implementation}{lem:weq-iso}
Given an equivalence $f: X\to Y$ we can take $g \defeq f^{-1}$.
For the converse, see Chapter~4 of the HoTT Book,\footcite{hottbook} or \coqident{Foundations.PartA}{isweq_iso}.
\end{implementation}

We put \cref{lem:weq-iso} immediately to good use.

\begin{lemma}\label{lem:contract-away}
Let $X$ be a type with element $a$, and let
$B(x,i)$ be a type for all $x:X$ and $i: a \eqto x$.
Define $f(x,i): B(x,i) \to B(a,\refl{a})$ by induction on $i$,
setting $f(a,\refl{a},b) \defeq b$ for all $b:B(a,\refl{a})$.
Then $f$ defines an equivalence
\[
f~:~ \sum_{x:X} \sum_{i: a \eqto x} B(x,i) \quad \to \quad B(a,\refl{a}).
\]
\end{lemma}
\begin{proof}
We can also define
$g: B(a,\refl{a})\to \sum_{x:X} \sum_{i: a \eqto x} B(x,i)$
mapping $b: B(a,\refl{a})$ to $(a,\refl{a},b)$.
Clearly $f(g(b)) \eqto b$ for all $b:B(a,\refl{a})$.
Moreover, $g(f(x,i,b)) \eqto (x,i,b)$ is clear by induction
on $i$, for all $b:B(x,i)$.
By \cref{lem:weq-iso} it follows that $f$
is an equivalence.
\end{proof}

The above lemma clearly reflects the  contractibility of the
singleton type $\sum_{x:X}(a \eqto x)$.\footnote{%
  In fact, an alternative proof would go as follows:
  \label{ft:Sigma-assoc}
  First, we use \cref{lem:weq-iso} to construct an element of
  $\sum_{x:X}\sum_{y:Y(x)}Z(x,y)
  \equivto \sum_{w : (\sum_{x:X}Y(x))}Z(\fst w,\snd w)$, i.e.,
  the associativity of sum types, where $X$ is a type,
  $Y(x)$ is a family of types depending on $x:X$,
  and $Z(x,y)$ is a family of types depending on $x:X$ and $y:Y(x)$.
  Then, we construct for any contractible type $X$
  and for any family of types $Y(x)$ depending on $x:X$,
  an equivalence between $\sum_{x:X}Y(x)$ and $Y(c)$,
  where $c$ is the center of contraction of $X$.}
For this reason
we call application of this lemma `to contract away'
the prefix $\sum_{x:X} \sum_{i: a \eqto x}$, in order
to obtain a simpler type. It is often applied
in the following simpler form.

\begin{corollary}\label{cor:contract-away}
With conditions as above, but with $B$ not depending on $i$, the same $f$
establishes an equivalence
\[
 \sum_{x:X} ((a \eqto x)\times B(x))~~\equivto~~B(a).
\]
\end{corollary}

In the direction of further generality, we offer the following exercise.
\begin{xca}\label{xca:sum-equiv-base}
  Suppose $X,Y$ are types related by an equivalence $f : X \to Y$.
  Let $B(x)$ be a type for all $x:X$. Construct an equivalence between
  $\sum_{x:X}B(x)$ and $\sum_{y:Y}B(\inv{f}(y))$.
\end{xca}
We proceed now to define the notion of fiberwise equivalence.

\begin{definition}\label{def:fiberwise}
Let $X$ be a type, and let $Y(x),Z(x)$ be families of types parametrized
by $x:X$. A map $f$ of type $\prod_{x:X}(Y(x)\to Z(x))$
can be viewed as a family of maps $f(x): Y(x)\to Z(x)$ and is called a
\emph{fiberwise} map. The \emph{totalization} of $f$ is defined by
$\tot(f)(x,y)\defeq (x,f(x)(y))$.
\index{totalization}
\glossary(totalization){$\protect\tot(f)$}{totalization of $\protect f$}
Using the denotation $\Tot(\blank)$ for the total type of
a type family we thus have
\[
  \tot(f) : \Tot(Y) \to \Tot(Z)).\qedhere
\]
\end{definition}

\begin{lemma}\label{lem:fiberwise}
Let conditions be as in \cref{def:fiberwise}.
If $f(x): Y(x) \to Z(x)$ is an equivalence for every $x:X$
(we say that $f$ is a \emph{fiberwise} equivalence),
%in which case we also call the family $f$ an equivalence,
then $\tot(f)$ is an equivalence.
\end{lemma}
\marginnote{We will allow ourselves to drop the ``fiberwise'' and talk simply about maps and equivalences between type families.}
\begin{proof}
If $f(x): Y(x) \to Z(x)$ is an equivalence for all $x$ in $X$,
then the same is true of all $f(x)^{-1}: Z(x) \to Y(x)$.
Then we have the totalization $\tot(x\mapsto f(x)^{-1})$,
which can easily be proved to be an inverse of $\tot(f)$
(see the next exercise). Now apply \cref{lem:weq-iso}.
\end{proof}

\begin{xca}\label{xca:fiberwise}
Complete the details of the proof of \cref{lem:fiberwise}.
\end{xca}

The converse to \cref{lem:fiberwise} also holds.
\begin{lemma}\label{lem:fiberwise-equiv-from-tot}
  Continuing with the setup of \cref{def:fiberwise},
  if $\tot(f)$ is an equivalence, then $f$ is a fiberwise equivalence.
\end{lemma}
For a proof see~Theorem~4.7.7 of the HoTT Book\footcite{hottbook}.

Yet another application of the notion of equivalence is to postulate axioms.

\begin{principle}\label{def:funext}
The axiom of \emph{function extensionality} postulates that the function
$\ptw_{f,g}: (f \eqto g) \to \prod_{x:X} f(x) \eqto g(x)$ in \cref{def:ptw} is an equivalence.
Formally, we postulate the existence of an element $\funext : \isEq(\ptw_{f,g})$.
From that we can construct the corresponding inverse function
\[
\inv{\ptw}_{f,g}: \Bigl(\prod_{x:X} f(x) \eqto g(x)\Bigr) \to (f \eqto g).
\]
Thus two functions whose values can all be identified can themselves be identified.
This supports the intuition that there is nothing more to a function than the values
it sends its arguments to.
\end{principle}

\begin{xca}\label{xca:Xequiv1toX}
  Let $X$ be a type.  Construct an equivalence of type $( \true \to X ) \equivto X $.
\end{xca}

\begin{xca}\label{xca:XequivXtimes1}
  Let $X$ be a type, and regard $\true$ as a constant family of types over $X$.
  Construct an equivalence of type $( \sum_{x:X} \true ) \equivto X $.
\end{xca}

\begin{xca}\label{xca:Sigma-distrib}
  Let $X$ and $Y$ be types, and let $Z(y)$ be a type parameterized by $y:Y$.
  Construct an equivalence of type
  $\bigl(X\times\sum_{y:Y}Z(y)\bigr) \equivto \sum_{y:Y}(X\times Z(y))$.
\end{xca}

\begin{xca}\label{xca:Sigma-comm}
  Let $X$ and $Y$ be types, and let $Z(x,y)$ be a type parameterized by
  $x:X$ and $y:Y$.
  Construct an equivalence of type $\bigl(\sum_{x:X}\sum_{y:Y}Z(x,y)\bigr)
  \equivto \sum_{y:Y}\sum_{x:X}Z(x,y)$.
\end{xca}

\begin{xca}\label{xca:fib-of-comp}
  Let $X$, $Y$ and $Z$ be types. Given functions $f: X\to Y$ and $g: Y\to Z$,
  construct a family of equivalences of type
  $\inv{(gf)}(z) \equivto \sum_{w:\inv{g}(z)}\inv{f}(\fst w)$ parameterized
  by $z:Z$. Hint: use \cref{ft:Sigma-assoc}.
\end{xca}

\begin{xca}\label{xca:AC-in-TT}
  Let $X$ and $Y$ be types, and let $Z(x,y)$ be a type parameterized by
  $x:X$ and $y:Y$.
  Construct an equivalence of type $\bigl(\prod_{x:X}\sum_{y:Y}Z(x,y)\bigr)
  \equivto \sum_{f:X\to Y}\prod_{x:X}Z(x,f(x))$.\footnote{%
    This equivalence is sometimes called the type-theoretic axiom of choice;
    more prosaically, it expresses the distributivity of products ($\Pi$-types)
    over sums ($\Sigma$-types).
    We discuss the real axiom of choice in~\cref{sec:choicefin}.}
\end{xca}

\begin{xca}\label{xca:section-above-f}
  Let $X$ and $Z$ be types, and let $Y(x)$ be a type parameterized by $x:X$.
  For any function $f:Z\to X$, construct an equivalence
  of type $\bigl(\prod_{z:Z}Y(f(z))\bigr)\equivto 
  \sum_{g:Z\to\sum_{x:X}Y(x)}(f\eqto \fst\circ g)$.\footnote{%
  The special case $Z\jdeq X$, $f\jdeq\id_X$ applies to any product type.}
\end{xca}

\begin{xca}\label{xca:Sigma-curry}\index{currying}
  Let $X$ and $Z$ be types, and let $Y(x)$ be a type parameterized by $x:X$.
  Construct an equivalence\footnote{%
  This canonical equivalence is often called ``currying'',
  after Haskell B.~Curry, and will be treated transparently, \ie
  we will pass between $f(x,y)$ and $f(x)(y)$ without denoting it.
  Note that the equivalence goes between
  $(X\times Y)\to Z$ and $X\to(Y\to Z)$ in case $Y(x)$ is constant.
  }
  of type $\bigl((\sum_{x:X}Y(x))\to Z\bigr)\equivto \prod_{x:X}(Y(x)\to Z)$.
\end{xca}

\section{Identifying pairs}\label{sec:pairpaths}

The identity type of two elements of $\sum _{x:X} Y(x)$ is inductively defined in \cref{sec:identity-types}, as for any other type, but
one would like to express the identity type for pairs in terms of identifications in the constituent types.  This would explain better what it means for
two pairs to be identified.  We start with a definition.

\begin{definition}\label{def:pairtopath}
  Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.\marginnote{%
    We picture paths between pairs much in the same way as
    paths over paths, cf.~\cref{ft:path-over-pic}.
    Just as, to give a pair in the sum type $\sum_{x:X}Y(x)$,
    we need both the point $x$ in the parameter type $X$
    as well as the point $y$ in $Y(x)$,
    to give a path from $(x,y)$ to $(x',y')$,
    we need both a path $p : x \eqto x'$
    as well as a path $q : \pathover y Y p {y'}$ over $p$.
    Here's a similar picture, where we depict the types in the family
    as being $2$-dimensional for a change.
    \begin{tikzpicture}
    % Name the coordinates so they are easy to change
    % first: X
    \coordinate (X-left) at (-1,-1);
    \node[dot,label=below:$x$] (X-x) at (0,-1.2) {};
    \node[dot,label=below:$x'$] (X-xp) at (1.5,-.9) {};
    \coordinate (X-right) at (2.8,-1);
    \node (X) at (3,-1) {$X$};
    \draw (X-left) .. controls +(-10:.3) and +(0:-.3) .. (X-x);
    \draw[->] (X-x) .. controls +(0:.3) and +(-10:-.5) ..
      node[anchor=north] {$p$} (X-xp);
    \draw (X-xp) .. controls +(-10:.5) and +(0:-.1) .. (X-right);
    % cylinder
    \coordinate (Y-top-left) at (-1,2);
    \coordinate (Y-bot-left) at (-1,0);
    \coordinate (Y-top-x) at (0,1.9);
    \coordinate (Y-center-x) at (0,1);
    \coordinate (Y-bot-x) at (0,0.1);
    \coordinate (Y-top-xp) at (1.5,2.1);
    \coordinate (Y-center-xp) at (1.5,1.1);
    \coordinate (Y-bot-xp) at (1.5,0.1);
    \coordinate (Y-top-right) at (2.8,2);
    \coordinate (Y-bot-right) at (2.8,0.2);
    \draw (Y-top-left) arc (90:450:.2 and 1);
    \fill[opacity=0.6,casred] (Y-center-x) ellipse (.18 and .9);
    \fill[opacity=0.6,casblue] (Y-center-xp) ellipse (.2 and 1);
    \draw (Y-top-x) arc (90:-90:.18 and .9);
    \draw[dashed] (Y-top-x) arc (90:270:.18 and .9);
    \draw (Y-top-xp) arc (90:-90:.2 and 1);
    \draw[dashed] (Y-top-xp) arc (90:270:.2 and 1);
    \draw (Y-top-right) arc (90:-90:.18 and .9);
    \draw[dashed] (Y-top-right) arc (90:270:.18 and .9);
    \draw (Y-top-left) .. controls +(-10:.3) and +(0:-.3) ..
      (Y-top-x) .. controls +(0:.3) and +(-10:-.5) ..
      (Y-top-xp) .. controls +(-10:.5) and +(0:-.1) .. (Y-top-right);
    \draw (Y-bot-left) .. controls +(-10:.3) and +(0:-.3) ..
      (Y-bot-x) .. controls +(0:.3) and +(-10:-.5) ..
      (Y-bot-xp) .. controls +(-10:.5) and +(0:-.1) .. (Y-bot-right);
    % Now the specifics: two points y,y' and the pathover
    \begin{scope}[label distance=2pt]
      \node[dot,label=left:$y$] (y) at (0,0.9) {};
      \node[dot,label=right:$y'$] (yp) at (1.5,1.1) {};
    \end{scope}
    \draw[->] (y) .. controls +(0:.5) and +(0:-.5) ..
      node[anchor=south] {$q$} (yp);
    \end{tikzpicture}}
  Consider the function
  \[
    \pair : \prod_{x:X} \Bigl( Y(x) \to \sum _{x':X} Y(x') \Bigr)
  \]
  defined by
  \[
    \pair(x)(y) \defeq (x,y).
  \]
  For any elements $(x,y)$ and $(x',y')$ of $\sum _{x:X} Y(x)$, we define the map
  \[
    \Bigl( \sum_{p:x \eqto x'} \pathover y Y p {y'} \Bigr)
    \to \left ( (x,y) \eqto (x',y') \right )
  \]
  by
  \[
    (p,q) \mapsto \apap {\pair} p q.
  \]
  (Refer to \cref{def:pathsoverpaths} for the meaning of the type $\pathover y Y p {y'}$, and to \cref{def:applfun2} for the definition of $\constant{apap}$.)
  We introduce $\pathpair p q$ as notation for $\apap {\pair} p q$.
\end{definition}

\begin{construction}\label{cor:isEq-pair=}
  In the situation of \cref{def:pairtopath}, if $x'$ is $x$,
  so that we have $( \pathover y Y {\refl x} {y'} ) \jdeq ( y \eqto y' )$,
  then for any $q : y \eqto y'$, we can construct an identification of type:
  \[
    \pathpair {\refl x} q \eqto \ap {\pair (x)} q
  \]
\end{construction}

\begin{implementation}{cor:isEq-pair=}
  By induction on $q$ it suffices to establish an identification
  \[
    \pathpair {\refl x} {\refl y} \eqto \ap {\pair (x)} (\refl y),
  \]
  both sides of which are
  equal to $\refl {(x,y)}$ by definition.
\end{implementation}

The following lemma gives the desired characterization of paths between pairs.

\begin{lemma}\label{lem:isEq-pair=}
  Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
  For any elements $(x,y)$ and $(x',y')$ of $\sum _{x:X} Y(x)$,
  the map defined in \cref{def:pairtopath} defined by
  \[
    (p,q) \mapsto \pathpair p q
  \]
  is an equivalence of type
  \[
    \Bigl( \sum_{p:x \eqto x'} \pathover y Y p {y'} \Bigr)
    \equivto \bigl( (x,y) \eqto (x',y') \bigr).
  \]
\end{lemma}

\begin{proof}
  Call the map $\Phi$.
  A map the other way,
  \[
    \Psi : ((x,y) \eqto (x',y')) \to \sum_{p:x \eqto x'} \pathover y Y p {y'},
  \]
  can be defined by induction, by setting
  \[
    \Psi (\refl {(x,y)}) \defeq (\refl x, \refl y).
  \]
  One proves, by induction on paths, the identifications $ \Psi ( \Phi (p,q) ) \eqto (p,q) $ and $ \Phi (\Psi ( r )) \eqto r$, so $\Psi$ and $\Phi$ are inverse functions.
  Applying \cref{lem:weq-iso}, we see that $\Phi$ and $\Psi$ are inverse equivalences, thereby obtaining the desired result.
\end{proof}

We often use $\fst(\pathpair p q) \eqto p$ and $\snd(\pathpair p q) \eqto q$,
which follow by induction on $p$ and $q$ from the definitions of $\ap{}$ and $\pathpair \_ \_$.
Similarly, $r \eqto \pathpair {\fst(r)}{\snd(r)}$ by induction on $r$.

\section{Binary products}
\label{sec:binprod-types}

There is special case of sum types that deserves to be mentioned since
it occurs quite often. Let $X$ and $Y$ be types, and consider the constant
family of types $Y(x)\defeq Y$. In other words, $Y(x)$ is a type that depends
on an element $x$ of $X$ that happens to be $Y$ for any such $x$.
(Recall \cref{xca:trp-nondep}.)
Then we can form the sum type $\sum_{x:X} Y(x)$ as above.
Elements of this sum type are pairs $(x,y)$
with $x$ in $X$ and $y$ in $Y(x)\jdeq Y$.\footnote{%
  These \emph{cartesian} products we illustrate as usual
  by rectangles where one side represents $X$ and the other $Y$.\par
  \begin{tikzpicture}
    % X
    \coordinate (X-left) at (-.5,-1);
    \node[dot,label=below:$x$] (X-x) at (1.2,-1) {};
    \coordinate (X-right) at (2.5,-1);
    \node (X) at (2.9,-1) {$X$};
    \draw (X-left) -- (X-right);
    % Y
    \coordinate (Y-bot) at (3.5,0);
    \node[dot,label=right:$y$] (Y-y) at (3.5,1) {};
    \coordinate (Y-top) at (3.5,2);
    \node (Y) at (3.5,-.4) {$Y$};
    \draw (Y-top) -- (Y-bot);
    % XY
    \node (SXY) at (.4,.5) {${X\times Y}$};
    \coordinate (XY-top-left) at (-.5,2);
    \coordinate (XY-bot-left) at (-.5,0);
    \coordinate (XY-top-x) at (1,2);
    \coordinate (XY-bot-x) at (1,0);
    \coordinate (XY-y-left) at (0,1);
    \coordinate (XY-y-right) at (2.5,1);
    \coordinate (XY-top-right) at (2.5,2);
    \coordinate (XY-bot-right) at (2.5,0);
    \draw (XY-bot-left) -- (XY-bot-right) -- (XY-top-right)
    -- (XY-top-left) --cycle;
    \draw[dashed] (1.2,0) -- (1.2,2);
    \draw[dashed] (-.5,1) -- (2.5,1);
    \node[dot,label=above left:${(x,y)}$] (xy) at (1.2,1) {};
    \draw[->,shorten <=.1cm,shorten >=.1cm] (1.2,0)
    -- node[anchor=east] {${\fst}$} (X-x);
    \draw[->,shorten <=.1cm,shorten >=.1cm] (2.5,1)
    -- node[anchor=south] {${\snd}$} (Y-y);
  \end{tikzpicture}}
In this case the type of $y$
doesn't depend on $x$, and in this special case the sum type is called
the \emph{binary product}, or \emph{cartesian product} of the types $X$ and $Y$,
denoted by $X \times Y$.
\index{type!binary product}\index{type!cartesian product}
\glossary(2times){$\times$}{cartesian product of two types}

At first glance, it might seem odd that a sum is also a product, but exactly the same thing happens with numbers, for the sum $5+5+5$ is also
referred to as the product $3 \times 5$.  Indeed, that's one way to define $3 \times 5$.

Recall that we have seen something similar with the product type $\prod_{x:X} Y(x)$, which we let $X \to Z$ denote in the case where $Y(x)$ is a
constant family of the form $Y(x)\defeq Z$, for some type $Z$.

The type $X \times Y$ inherits the functions $\fst,\snd$ from
$\sum_{x:X} Y(x)$, with the same definitions $\fst(x,y)\defeq x$
and $\snd(x,y)\defeq y$. Their types can now be denoted in a
simpler way as $\fst: (X \times Y)\to X$ and
$\snd: (X \times Y)\to Y$, and they are called as before the
first and the second projection, respectively.

Again, proving something about (or constructing something from) every
element $(a,b)$ of $X \times Y$ is simply done for all $a:X$ and $b:Y$.

There is an equivalence between $(a_1,b_1) \eqto (a_2,b_2)$ and $(a_1 \eqto a_2) \times (b_1 \eqto b_2)$.
This follows from \cref{lem:isEq-pair=} together with \cref{xca:trp-nondep}.

If $f: X \to Y$ and $f': X' \to Y'$, then we let
$f\times f'$ denote the map of type $(X\times X') \to (Y\times Y')$
that sends $(x,x')$ to $(f(x),f'(x'))$.

The following lemma follows from \cref{lem:isEq-pair=}, combined with \cref{def:pathover-trp} and \cref{xca:trp-nondep}.

\begin{lemma}\label{lem:isEq-pair-bin=}
  Suppose we are given type $X$ and $Y$.
  For any elements $(x,y)$ and $(x',y')$ of $X \times Y$,
  the map defined in \cref{def:pairtopath} defined by
  \[
    (p,q) \mapsto \pathpair p q
  \]
  is an equivalence of type
  \[
    ( x\eqto x' ) \times (y\eqto y') \equivto \left( (x,y)\eqto (x',y')\right).
  \]
\end{lemma}

\begin{xca}\label{xca:binary-prod-equiv}
  Let $X,Y$ be types in a universe $\UU$, and consider the type family
  $T(z)$ in $\UU$ depending on $z:\bool$ defined by
  $T(\no)\defeq X$ and $T(\yes) \defeq Y$.
  Show that the function $(\prod_{b:\bool}T(b))\to X\times Y$
  sending $f$ to $(f(\no),f(\yes))$, is an equivalence.
\end{xca}

\begin{xca}\label{xca:binary-prod-comm}
  Let $X$ and $Y$ be types.
  Construct an equivalence of type $(X \times Y) \equivto (Y\times X)$.
\end{xca}

\section{More inductive types}
\label{sec:inductive-types}

There are other examples of types that are conveniently introduced
in the same way as we have seen with the natural numbers and the identity types.
A type
presented in this style shares some common features: there are some ways to create new elements, and there is a way (called \emph{induction}) to
prove something about every element of the type (or family of types).  We will refer to such types as \emph{inductive} types, and we present a
few more of them in this section, including the finite types, and then we present some other constructions for making new types from old ones.
For each of these constructions we explain the identity type for two
elements of the newly constructed type in terms of identity types for
elements of the constituent types.

\subsection{Finite types}
\label{sec:finite-types}
Firstly, there is the \emph{empty} type in the universe $\UU_0$, denoted by $\emptytype$ or by $\false$.  It is an inductive type, with no way
to construct elements of it.  The induction principle for $\emptytype$ says that to prove something about (or to construct something from) every
element of $\emptytype$, it suffices to consider no special cases (!).
Hence, every statement about an arbitrary element of $\emptytype$ can be
proven. (This logical principle is traditionally called
\emph{ex falso (sequitur) quodlibet}.\footnote{%
From falsehood, anything follows. Also called the principle of explosion.})
As an example, we may prove that any two elements $x$ and $y$ of
$\emptytype$ are equal (i.e., construct an identification of
type $x\eqto y$) by using induction on $x$. We may even
prove by induction on $x:\emptytype$ that the elements
$0$ and $\Succ(0)$ of $\NN$ are equal
(i.e., construct a function of type $\emptytype\to(0\eqto\Succ(0)$).

An element of $\emptytype$ will be called an \emph{absurdity}.  Of course, one expects that there are no real absurdities in mathematics, nor in any
logical system (such as ours) that attempts to provide a language for mathematics, but it is important to have such a name so we can discuss
the possibility, which might result inadvertently from the introduction of unwarranted assumptions.  For example, to assert that a type $T$ has
no elements, it would be sensible to assert that an element of $T$ would lead to an absurdity.  Providing a function of type $T \to \emptytype$ is a
convenient way to make that assertion.

Secondly, there will also be an inductive type called $\true$ in the universe $\UU_0$ provided with a single element $\triv$; (the name $\triv$
comes from the word ``trivial'').  Its induction principle states that, in order to prove something about (or to construct something from) every
element of $\true$, it suffices to consider the special case where the element is $\triv$.  As an example, we may construct, for any element
$u : \true$, an identification of type $u \eqto \triv$; we use induction to reduce to the case where $u$ is $\triv$, and then $\refl{\triv}$ provides the
desired element.  One may also construct, for any elements $x$ and $y$ of $\true$, an identification of type $x \eqto y$ by using induction both on $x$ and
on $y$.

There is a function $X \to \true$, for any type $X$, namely: $a \mapsto \triv$.  This corresponds, for propositions, to the statement that an
implication holds if the conclusion is true.

\begin{xca}\label{xca:True-univ-prop}
  Let $X$ be a type. Define the function $e$ of type
  $(\true\to X) \to X$ by $e(f)\defeq f(\triv)$.
  Prove that $e$ is an equivalence.
  This is called \emph{the universal property of} $\true$.
\end{xca}

Thirdly, there will be an inductive type called $\bool$ in the universe $\UU_0$, provided with two elements, $\yes$ and $\no$.  Its induction
principle states that, in order to prove something about (or to construct something from) every element of $\bool$, it suffices to consider two
cases: the special case where the element is $\yes$ and the special case where the element is $\no$.

We may use substitution to construct an element of type
$(\yes \eqto \no)\to \emptytype$, expressing that the identification
of $\yes$ with $\no$ leads to an absurdity.
To do this, we introduce a family of types $P(b)$ in the universe
$\UU_0$ parametrized by a variable $b:\bool$.  We define $P(b)$ by induction on $b$ by setting $P(\yes) \defeq \true$ and
$P(\no) \defeq \false$.  (The definition of $P(b)$ is motivated by the expectation that we will be able to construct an equivalence between $P(b)$ and
$\yes \eqto b$.)  If there were an element $e: \yes \eqto \no$, we could substitute $\no$ for $\yes$ in $\triv : P (\yes)$ to get an element of $P(\no)$,
which is absurd.  Since $e$ was arbitrary, we have defined a function $(\yes \eqto \no) \to \emptytype$, as desired.

In the same way, we may use substitution to prove that it is absurd
that successors of natural numbers are identical to $0$,
\ie for any $n:\NN$ that $(0 \eqto \Succ(n))\to \emptytype$.
To do this, we introduce a family of types $P(i)$ in $\UU_0$ parametrized
by a variable $i:\NN$.  Define $P$ recursively by
specifying that $P(0) \defeq \true$ and $P(\Succ(m)) \defeq \false$.  (The definition of $P(i)$ is motivated by the expectation that we will be
able to construct an equivalence between $P(i)$ and $0 \eqto i$.)  If there were an element $e: 0 \eqto \Succ(n)$, we could substitute $\Succ(n)$ for $0$
in $\triv : P ( 0 )$ to get an element of $P(\Succ(n))$, which is absurd.  Since $e$ was arbitrary, we have defined a function $(0 \eqto \Succ(n)) \to \emptytype$,
establishing the claim.

In a similar way we will in \cref{sec:typeFin} define types $\bn n$ for any $n$ in $\NN$
such that $\bn n$ is a type (set) of $n$ elements.


\subsection{Binary sums}
\label{sec:binsum-types}
For sum types of the form $\sum_{b:\bool} T(b)$, with $T(b)$
a type depending on $b$ in $\bool$, there is an equivalence with a simpler type.\footnote{%
  In a case like this, we can thicken up the lines denoting
  $T(\no)$ and $T(\yes)$ in our picture, if we like:\par
  \begin{tikzpicture}
    \node[dot,label=below:${\no}$] (no) at (0,-.8) {};
    \node[dot,label=below:${\yes}$] (yes) at (1.5,-.8) {};
    \node (Bool) at (2.5,-.8) {$\bool$};
    \draw (0,0.9) ellipse (.25 and 1);
    \node (Tno) at (0,2.2) {$T(\no)$};
    \draw (1.5,1.1) ellipse (.4 and 0.8);
    \node (Tyes) at (1.5,2.2) {$T(\yes)$};
    \node[dot,label=above:$x$] (x-no) at (0,0.8) {};
    \node[dot,label=below:$y$] (y-yes) at (1.5,1.2) {};
  \end{tikzpicture}}
After all, the type family $T(b)$ is fully determined
by two types, namely by the types $T(\no)$ and $T(\yes)$.
The elements of $\sum_{b:\bool} T(b)$ are dependent pairs $(\no,x)$ with
$x$ in $T(\no)$ and $(\yes,y)$ with $y$ in $T(\yes)$. The resulting
type can be viewed as the \emph{disjoint union} of $T(\no)$ and $T(\yes)$:
from an element of $T(\no)$ or an element of $T(\yes)$
we can produce an element of $\sum_{b:\bool} T(b)$.

These disjoint union types can be described more clearly in the following way.
The \emph{binary sum} of two types $X$ and $Y$, denoted
\glossary(2amalg){$\amalg$}{sum of two types}$X \amalg Y$,
is an inductive type with two constructors: $\inl{} : X \to X \amalg Y$ and
$\inr{} : Y \to X \amalg Y$.\footnote{%
  Beware that in a picture, the same point may refer
  either to $x$ in $X$ or to $\inl x$ in the sum $X \amalg Y$:\par
  \begin{tikzpicture}
    \draw (0,0.9) ellipse (.25 and 1);
    \node (X) at (0,2.1) {$X$};
    \draw (1,1.1) ellipse (.4 and 0.8);
    \node (Y) at (1,2.1) {$Y$};
    \node[dot,label=above:$x$] (x) at (0,0.8) {};
    \node[dot,label=below:$y$] (y) at (1,1.2) {};
    \draw[dashed] (0.5,1.1) ellipse (1.2 and 1.6);
    \node (XY) at (-0.75,2.35) {$X \amalg Y$};
  \end{tikzpicture}}
Proving a property of any element of $X \amalg Y$
means proving that this property holds of any $\inl{x}$ with $x:X$ and any
$\inr{y}$ with $y:Y$. In general, constructing a function $f$ of type
$\prod_{z: X \amalg Y} T(z)$, where $T(z)$ is a type depending on
$z$, is done by defining $f(\inl{x})$ for all $x$ in $X$
and $f(\inr{y})$ for all $y$ in $Y$.

\begin{xca}\label{xca:binary-sum-equiv}
  Let $X,Y$ be types in a universe $\UU$, and consider the type family
  $T(z)$ in $\UU$ depending on $z:\bool$ defined by induction on $z$ by
  $T(\no)\defeq X$ and $T(\yes) \defeq Y$.
  Show that the map $f : X\amalg Y \to \sum_{b:\bool}T(b)$,
  defined by $f (\inl x) \defeq (\no,x)$ and $f(\inr y) \defeq (\yes,y)$,
  is an equivalence.
\end{xca}

Identification of two elements $a$ and $b$ in $X \amalg Y$ is
only possible if they are constructed with the same constructor.
Thus $\inl{x} \eqto \inr{y}$ is always empty, and there are equivalences of type
$(\inl{x} \eqto \inl{x'}) \equivto (x \eqto x')$ and
$(\inr{y} \eqto \inr{y'}) \equivto (y \eqto y')$.

\begin{xca}\label{xca:binary-sum-id}
  Prove these statements using \cref{xca:binary-sum-equiv},
  \cref{lem:isEq-pair=}, and a characterization
  of the identity types of $\bool$.
\end{xca}

\begin{xca}\label{xca:bin-sum-univ-prop}
  Let $X$, $Y$, $Z$ be types. Define a function $e$ from
  $(X\amalg Y)\to Z$ to $(X\to Z)\times(Y\to Z)$ by precomposition
  with the constructors.
  Prove that $e$ is an equivalence.
  This is called \emph{the universal property of the binary sum}.
\end{xca}

\begin{xca}
  Let $X$ be a type.  Construct an equivalence of type $(X \amalg \emptytype) \equivto X$.
\end{xca}

\subsection{Unary sums}\label{sec:unary-sum-types}

Sometimes it is useful to be able to make a copy of a type $X$:
A new type that behaves just like $X$,
though it is not equal to $X$ by definition.
The \emph{unary sum} or \emph{wrapped copy} of $X$ is an inductive type $\Copy(X)$
with a single constructor, $\inc{} : X \to \Copy(X)$.\footnote{%
  A point $x:X$ corresponds to the point $\inc{x}:\Copy(X)$:\par
  \begin{tikzpicture}
    \draw (0,1) ellipse (.3 and .8);
    \draw[dashed] (-.1,1) ellipse (.6 and 1.1);
    \node[dot,label=above:$x$] (x) at (0,0.8) {};
    \node (X) at (-.45,.7) {$X$};
    \node (c) at (.75,1) {$\leftrightarrow$};
    \draw[dashed] (1.7,1) ellipse (.3 and .8);
    \draw (1.6,1) ellipse (.6 and 1.1);
    \node[dot,label=above:$\inc{x}$] (inx) at (1.7,0.8) {};
    \node (Xdashed) at (2.6,.1) {$\Copy(X)$};
  \end{tikzpicture}\par
  \noindent Note that $\Copy(X)$ can alternatively be defined as $\sum_{z:\true}X$.}
Constructing a function $f : \prod_{z:\Copy(X)}T(z)$,
where $T(z)$ is a type depending on $z : \Copy(X)$,
is done by defining $f(\inc{x})$ for all $x:X$.
Taking $T(z)$ to be the constant family at $X$,
we get a function, $\out : \Copy(X) \to X$,
called the \emph{destructor},
with $\out(\inc{x}) \defeq x$ for $x:X$,
and the induction principle implies that $\inc{\out(z)} \eqto z$
for all $z:\Copy(X)$, so there is an equivalence of type
$\Copy(X) \equivto X$, as expected.
It follows that there are equivalences of type
$(\inc{x} \eqto \inc{x'}) \equivto (x \eqto x')$ and
$(\out(z) \eqto \out(z')) \equivto (z \eqto z')$.

Note that we can make several copies of $X$ that are not
equal to each other by definition,
for instance, by picking different names for the constructor.
We write $\Copy_{\constructor{con}}(X)$ for a copy of $X$
whose constructor is
\[
  \constructor{con} : X \to \Copy_{\constructor{con}}(X).
\]

\begin{example}\label{exa:nnn}
Here's an example to illustrate why it can be useful to make such a wrapped type:
We introduced the natural numbers $\NN$ in \cref{sec:natural-numbers}.
Suppose we want a type consisting of negations of natural numbers,
$\set{\ldots, -2, -1,0}$,
perhaps as an intermediate step towards building the set of integers
$\set{\ldots, -2, -1,0,1,2,\ldots}$.\footnote{%
  We implement this in \cref{def:zet}.}
Of course, the type $\NN$ itself would do,
but then we would need to pay extra attention to whether $n:\NN$
is supposed to represent $n$ as an integer or its negation.
So instead we take the wrapped copy $\NNN\defeq\Copy_{-}(\NN)$,
with constructor ${-} : \NN \to \NNN$.%
\glossary(NNN){$\protect\NNN$}{the type of negated natural numbers,
  \cref{exa:nnn}}
We will also write ${-} : \NNN \to \NN$ for the destructor,
inductively defined by $-(-n)\defeq n$. (The ambiguity will
always be resolved by the types.) In fact, the constructor
and the destructor are each other's inverse since we
also have $-(-(-n))\jdeq -n$, and so by induction $-(-m) = m$ for all $m:\NNN$.
By \cref{lem:weq-iso} we get that they are equivalences.
\end{example}

\section{Univalence}\label{sec:univax}

The univalence axiom, to be presented in this section, greatly enhances
our ability to produce identifications between the two types and to use the
resulting identifications to transport (in the sense of \cref{def:transport})
properties and structure between the types.  It asserts that if $\UU$
is a universe, and $X$ and $Y$ are types in $\UU$, then a specific function,
mapping identifications between $X$ and $Y$ to equivalences between
$X$ and $Y$, is an equivalence.

We now define the function that the univalence axiom postulates
to be an equivalence.

\begin{definition}\label{def:idtoeq}
  For types $X$ and $Y$ in a universe $\UU$ and a path $p : X \eqto Y$,
  transport along $p$ in the type family $\id_\UU$ is a function
  from $X$ to $Y$. We recall the definition by path induction
  from \cref{def:transport}, setting $\trp[\id_\UU]{\refl{X}}\defeq\id_X$.
  As observed in \cref{sec:equivalence}, transport functions are
  equivalences, so that the result is a function
  \[
    (p\mapsto \trp[\id_\UU]{p}) : (X \eqto Y) \to (X\equivto Y).
    \qedhere
  \]
\end{definition}
We may write $\trp[\id_\UU]{p}$ more briefly as $\ptoe p$,%
\glossary(1trp){$\protect\ptoe p$}{transport between types along a path}
which we also use to denote the corresponding function of type $X\to Y$,
instead of $X\equivto Y$.

We are ready to state the univalence axiom.

\begin{principle}[Univalence Axiom]\label{def:univalence}
    Let $\UU$ be a universe.
    Voevodsky's \emph{univalence axiom}\index{univalence axiom} for $\UU$
    postulates that $p\mapsto \ptoe p$ is an equivalence
    of type $(X \eqto Y) \to (X\equivto Y)$, for all $X,Y:\UU$.
    Formally, we postulate the existence of a family of elements
    \[
      \ua_{X,Y} : \isEq((p:X\eqto Y)\mapsto \trp[\id_\UU]{p})
    \]
    \glossary(ua){$\protect\ua_{X,Y}$}%
    {postulated element of the univalence axiom}%
    parameterized by $X,Y:\UU$.
\end{principle}

For an equivalence $f: X\equivto Y$, we will adopt the
notation $\etop f : X \eqto Y $ to denote $\inv{(p\mapsto\ptoe p)}(f)$,%
\glossary(1bar){$\protect\etop f$}{path obtained by univalence from $f$}
the result of applying the inverse function of $(p\mapsto\ptoe p)$,
given by $\ua_{X,Y}$, to $f$.
Thus there are identifications of type $\etop {\ptoe p} \eqto p$
and $\ptoe {\etop f} \eqto f$.  There are also identifications of
type $\overetop{\id_X} \eqto \refl{X}$
and $\overetop{g\,f} \eqto \etop{g}\,\etop{f}$ if $g: Y\equivto Z$.

\begin{xca}\label{xca:C2}
Prove that $\bool \eqto \bool$ has exactly two elements,
$\refl{\bool}$ and $\swap$ (where $\swap$ is given by
univalence from the equivalence $\bool\to\bool$ interchanging (swapping)
the two elements of $\bool$), and that $\swap\cdot\swap \eqto \refl{\bool}$.%
\glossary(swap){$\protect\swap$}{interchange the elements of $\bool$,
  \cref{xca:C2}}
\end{xca}


\section{Heavy transport}
\label{sec:heavy-transport}

In this section we collect useful results on transport in
type families that are defined by a type constructor applied
to families of types.
Typical examples of such `structured' type families are
$Y(x)\to Z(x)$ and $x \eqto x$ parametrized by $x:X$.

\begin{definition}\label{def:function-type-families}
Let $X$ be a type, and let $Y(x)$ and $Z(x)$ be families of types parametrized by a variable $x:X$.
Define $Y\to Z$ to be the type family
with $(Y\to Z)(x) \defeq Y(x)\to Z(x)$.
\end{definition}
Recall from \cref{def:fiberwise} that an element $f : \prod_{x:X}(Y\to Z)(x)$
is called a fiberwise map,
and $f$ is called a fiberwise equivalence,
if $f(x): Y(x)\to Z(x)$ is an equivalence for all $x:X$.

\begin{construction}\label{lem:trp-in-function-type}
Let $X$ be a type, and let $Y(x)$ and $Z(x)$ be types for every $x:X$.
Then we have for every $x,x':X$, $e: x \eqto x'$, $f: Y(x)\to Z(x)$, and $y':Y(x')$ (see the diagram in the margin):%
\marginnote[-3\baselineskip]{%
  \begin{tikzcd}[column sep=huge,ampersand replacement=\&]
    x\ar[d,eql,"e"'] \&[-25pt]
    Y(x) \ar[r,"f"]\ar[d,equivl,"{\trp[Y]{e}}"'] \& Z(x)
    \ar[d,equivr,"{\trp[Z]{e}}"] \\
    x'\&[-25pt]
    Y(x') \ar[r,"{\trp[Y\to Z]{e}(f)}"'] \& Z(x')
  \end{tikzcd}}
\[
\trp[Y\to Z]{e}(f)(y') \eqto \trp[Z]{e} \Bigl(f\bigl(\trp[Y]{e^{-1}}(y')\bigr)\Bigr).
\]
\end{construction}
\begin{implementation}{lem:trp-in-function-type}
By induction on $e: x \eqto x'$. For $e \jdeq \refl{x}$, we have $e^{-1}\jdeq \refl{x}$,
and all transports are identity functions of appropriate type.
\end{implementation}

An important special case of the above lemma is with $\UU$
as parameter type and type families $Y\defeq Z\defeq \id_\UU$.
Then $Y\to Z$ is $X \mapsto (X\to X)$. Now,
if $A,B:\UU$ and $e: A \eqto B$ comes from an equivalence $g:A\equivto B$
by applying the univalence axiom,
then the above construction combined with function extensionality
yields that for any $f: A\to A$ (see the diagram in the margin)
\[
\trp[X \mapsto (X\to X)]{\etop g} (f) \eqto g\circ f \circ g^{-1}.
\]
\marginnote[-3\baselineskip]{%
  Transport using univalence:
  \begin{tikzcd}[column sep=huge,ampersand replacement=\&]
    A\ar[d,eql,"\etop g"'] \&[-25pt]
    A \ar[r,"f"]\ar[d,equivl,"g"'] \& A \ar[d,equivr,"g"] \\
    B\&[-25pt]
    B \ar[r,"\trp{\etop g}(f)"'] \& B
  \end{tikzcd}}

The following construction is implemented by induction on $e: x \eqto x'$.

\begin{construction}\label{lem:trp-in-fx=Ygx}
Let $X,Y$ be types, $f,g: X\to Y$ functions, and let
$Z(x)\defeq (f(x) \eqto g(x))$ for every $x:X$.
Then for all $x,x'$ in $X$, $e: x \eqto x'$, and $i: f(x) \eqto g(x)$ we have:
\[
\trp[Z]{ e} (i) \eqto \ap{g}(e) \cdot i \cdot \ap{f}(e)^{-1}.
\]
\end{construction}

\begin{xca}\label{xca:trp-in-a/x=b/x}
Implement \cref{lem:trp-in-fx=Ygx} in the following special cases,
where $Y\jdeq X$ and $a,b$ are elements of $X$:
\begin{enumerate}
\item $\trp[x\mapsto a \eqto b]{e} (i) \eqto i$;
\item\label{trp-in-a=x} $\trp[x\mapsto a \eqto x]{e} (i) \eqto e\cdot i$;
\item\label{trp-in-x=a} $\trp[x\mapsto x \eqto b]{e} (i) \eqto i \cdot e^{-1}$;
\item\label{trp-in-x=x} $\trp[x\mapsto x \eqto x]{e} (i) \eqto e \cdot i\cdot e^{-1}$
(also called \emph{conjugation}).\qedhere
\end{enumerate}
\end{xca}

There is also a dependent version of \cref{lem:trp-in-fx=Ygx},
which is again proved by induction on $e$.\footnote{%
  We picture this in two stages. First, we show the fiberwise
  situation as follows:\par
  \noindent\begin{tikzpicture}
    % Name the coordinates so they are easy to change
    % first: X
    \coordinate (X-left) at (-1,-1);
    \node[dot,label=below:$x$] (X-x) at (0,-1.2) {};
    \node[dot,label=below:$x'$] (X-xp) at (1.5,-1.3) {};
    \coordinate[label=right:$X$] (X-right) at (3.2,-1.1);
    % then: Y top and bottom
    \coordinate (Y-top-left) at (-1,2.1);
    \coordinate (Y-bot-left) at (-1,0.5);
    \coordinate[label=above:$Y(x)$] (Y-top-x) at (0,2.4);
    \coordinate (Y-bot-x) at (0,-.1);
    \coordinate[label=above:$Y(x')$] (Y-top-xp) at (1.5,2.7);
    \coordinate (Y-bot-xp) at (1.5,-.4);
    \coordinate (Y-top-right) at (3.2,2.3);
    \coordinate (Y-bot-right) at (3.2,0.0);
    \draw (Y-bot-left) .. controls +(-90:.5) and +(0:-.5) .. (Y-bot-x)
    .. controls +(0:.5) and +(-10:-.5) .. (Y-bot-xp)
    .. controls +(-10:.5) and +(90:-.5) .. (Y-bot-right)
    -- (Y-top-right)
    .. controls +(90:.5) and +(0:.5) .. (Y-top-xp)
    .. controls +(0:-.5) and +(-10:.4) .. (Y-top-x)
    .. controls +(-10:-.4) and +(90:.5) .. (Y-top-left)
    -- (Y-bot-left);
    \draw[dashed] (Y-bot-x) -- (Y-top-x);
    \draw[dashed] (Y-bot-xp) -- (Y-top-xp);
    \draw (X-left) .. controls +(-10:.3) and +(0:-.3) .. (X-x);
    \draw[->] (X-x) .. controls +(0:.3) and +(-10:-.5) ..
      node[anchor=north] {$e$} (X-xp);
    \draw (X-xp) .. controls +(-10:.5) and +(0:-.1) .. (X-right);
    % Now the specifics: two sections f,g and path-overs and transports
    \coordinate (Y-f-left) at (-1,0.6);
    \coordinate (Y-g-left) at (-1,1.6);
    \coordinate[label=right:$f$] (Y-f-right) at (3.2,0.9);
    \coordinate[label=right:$g$] (Y-g-right) at (3.2,1.5);
    \node[dot,label=below left:$f(x)$] (fx) at (0,0.5) {};
    \node[dot,label=above left:$g(x)$] (gx) at (0,1.5) {};
    \node[dot,label=below right:$f(x')$] (fxp) at (1.5,0.7) {};
    \node[dot,label=above right:$g(x')$] (gxp) at (1.5,1.7) {};
    \node[dot,label=right:$\trp{e}(f(x))$] (tfx) at (1.5,-.1) {};
    \node[dot,label=right:$\trp{e}(g(x))$] (tgx) at (1.5,2.4) {};
    \draw[dotted] (Y-f-left) .. controls +(30:.3) and +(0:-.5) .. (fx);
    \draw[->] (fx) .. controls +(0:.5) and +(0:-.5) ..
      node[anchor=south] {$\apd{f}(e)$} (fxp);
    \draw[dotted] (fxp) .. controls +(0:.5) and +(-30:-.3) .. (Y-f-right);
    \draw[dotted] (Y-g-left) .. controls +(-30:.3) and +(0:-.5) .. (gx);
    \draw[->] (gx) .. controls +(0:.5) and +(0:-.5) ..
      node[anchor=north] {$\apd{g}(e)$} (gxp);
    \draw[dotted] (gxp) .. controls +(0:.5) and +(25:-.3) .. (Y-g-right);
    \draw[->] (fx) -- node[anchor=east] {$i$} (gx);
    \draw[->] (fxp) -- node[anchor=west] {${\trp{e}(i)}$} (gxp);
    \draw (tfx) -- (fxp); \draw (gxp) -- (tgx);
    \draw[mapsto,shorten <=3pt,shorten >=2pt] (fx)
    .. controls +(-45:.5) and +(0:-.4) .. (tfx);
    \draw[mapsto,shorten <=3pt,shorten >=2pt] (gx)
    .. controls +(45:.5) and +(20:-.4) .. (tgx);
  \end{tikzpicture}\par
  \noindent Here, there's not room to show all
  that's going on in the fiber $Y(x')$, so we illustrate that
  as follows:\par
  \noindent\begin{tikzpicture}
    \node (Yxp) at (0.1,2) {$Y(x')$};
    \draw (0,-1)
    .. controls ++(200:-1) and ++(180:1) .. (2.5,-1.8)
    .. controls ++(180:-1) and ++(270:1) .. (3.5,0)
    .. controls ++(270:-1) and ++(20:2)   .. (2,2)
    .. controls ++(20:-2)   and ++(90:1)  .. (-1,0.7)
    .. controls ++(90:-1)  and ++(200:1) .. (0,-1);
    \node[dot,label=below left:$f(x')$] (fxp) at (0.1,-.4) {};
    \node[dot,label=above left:$g(x')$] (gxp) at (0.1,.6) {};
    \node[dot,label=below right:$\trp{e}(f(x))$] (tfx) at (1.8,-.7) {};
    \node[dot,label=above right:$\trp{e}(g(x))$] (tgx) at (1.8,1.2) {};
    \draw[<-] (fxp) .. controls +(-20:.5) and +(10:-.5) .. (tfx);
    \draw[->] (fxp) -- node[auto] {$\trp[Z]{e}(i)$} (gxp);
    \draw[<-] (gxp) .. controls +(10:.5) and +(0:-.5) .. (tgx);
    \draw[->] (tfx) .. controls +(45:.5) and +(-45:.5) ..
    node[auto,swap] {$\ap{\trp[Y]{e}}(i)$} (tgx);
    \node (poapdf) at (1.1,-.2) {$\po_e\bigl(\apd{f}(e)\bigr)$};
    \node (poapdg) at (.9,1.35) {$\po_e\bigl(\apd{g}(e)\bigr)$};
  \end{tikzpicture}}

\begin{construction}\label{lem:trp-in-fx=Yxgx}
Let $X,Y(x)$ be types and $f(x),g(x): Y(x)$ for all $x:X$.
Let $Z(x)\defeq (f(x) \eqto g(x))$,
with the identification in $Y(x)$, for every $x:X$.
Then for all $x,x'$ in $X$, $e: x \eqto x'$, and $i: f(x) \eqto g(x)$ we have:
\[
  \trp[Z]{ e} (i) \eqto \po_e\bigl(\apd{g}(e)\bigr)
  \cdot \ap{\trp[Y]{e}}(i) \cdot \po_e\bigl(\apd{f}(e)\bigr)^{-1}.
\]
\end{construction}

The following construction will be used later in the book.

\begin{definition}\label{def:Dan's-lemma}
Let $X,Y(x)$ be types and $f(x): Y(x)$ for all $x:X$.
Given elements $x,x':X$ and a path $p : x \eqto x'$, we define an equivalence
$(\pathover{f(x)}{Y}{e}{f(x')}) \equivto (f(x) \eqto f(x))$.
We do this by inducion on $p$, using \cref{def:pathsoverpaths},
thereby reducing to the case $(f(x) \eqto f(x)) \equivto (f(x) \eqto f(x))$,
which we solve in the canonical way as before.
\end{definition}


\section{Propositions, sets and groupoids}
\label{sec:props-sets-grpds}

Let $P$ be a type.  The property that $P$ has at most one element may
be expressed by saying that any two elements are equal.
Hence it is encoded by $\prod_{a,b:P} (a \eqto b)$.
We shall call a type $P$ with that property a \emph{proposition},%
\index{proposition}
and its elements will be called \emph{proofs} of $P$.%
\index{proof!of a proposition}
We will use them for doing logic in type theory.
The reason for doing so is that the most relevant
thing about a logical proposition is whether it has a proof or not.
It is therefore reasonable to require for any type representing
a logical proposition that all its members are equal.

Suppose $P$ is a proposition.  Then English phrases such as ``$P$ holds'', ``we know $P$'', and ``we have shown $P$'', will all mean that we
have an element of $P$.  We will not use such phrases for types that are not propositions, nor will we discuss knowing $P$ conditionally with a
phrase such as ``whether $P$''.  Similarly, if ``$Q$'' is the English phrase for a statement encoded by the proposition $P$, then the English
phrases ``$Q$ holds'', ``we know $Q$'', and ``we have shown $Q$'', will all mean that we have an element of $P$.

Typically, mathematical properties expressed in English as \emph{adjectives} will be encoded by types that are propositions, for in English
speech, when you assert that a certain adjective holds, you are simply asserting it, and not providing further information.  Examples: the
number $6$ is \emph{even}; the number $7$ is \emph{prime}; the number $28$ is \emph{perfect}; consider a \emph{regular} pentagon; consider an
\emph{isosceles} triangle.

Sometimes adjectives are used in mathematics, not to refer to properties of an object, but to modify the meaning of a noun, producing a
different noun phrase denoting a different mathematical concept.  For example, a \emph{directed} graph is a graph, each of whose edges is given
a bit of additional information: a direction in which it points.  Other examples: \emph{differentiable} manifold; \emph{bipartite} graph;
\emph{vector} space; \emph{oriented} manifold.

Let $X$ be a type.  If for any $x:X$ and any $y:X$ the identity
type $x \eqto y$ is a proposition, then we shall say that $X$ is a \emph{set}.%
\index{set}
The reason for doing so is that the most relevant
thing about a set is which elements it has; distinct identifications
of equal elements are not relevant.
Alternatively, we shall say that $X$ is a $0$-\emph{type}.\footnote{%
Sets are thought to consist of points. Points are entities of dimension 0,
which explains why the count starts here.
One of the contributions of Vladimir Voevodsky is the extension of
the hierarchy downwards, with the notion of proposition,
including logic in the same hierarchy.
Some authors therefore call propositions \emph{$(-1)$-types},
and they call contractible types \emph{$(-2)$-types}.}

The following definition introduces notational alternatives
commonly used in mathematics.

\begin{definition}\label{def:neg-eq-ne}
  Let $P$ be a proposition as defined above.
  We define the \emph{negation} of $P$\glossary(1neg){$\neg P$}{negation of a proposition $P$}
  by setting $\neg P \defeq (P \to \emptytype)$.

  Let $A$ be a \emph{set}, as defined above,
  and let $a$ and $b$ be elements of $A$.
  We write $a \eq b$\glossary(2=){$=$}{equality} as alternative
  notation for the type $a \eqto b$.  Formally, we define it as follows.
  \[
  (a \eq b) \defeq (a \eqto b)
  \]
  The type $a \eq b$ is called an \emph{equation}\index{equation}.
  When it has an element, we say that $a$ and $b$ are \emph{equal}.
  In line with this definition we also define the type
  $(a \ne b) \defeq \neg (a \eq b)$; an element of it asserts
  that the elements $a$ and $b$ of the set $A$ are not equal.
\end{definition}

Equations are propositions, so we can speak of them being true or false, and we may use them after the words \emph{if}, \emph{since},
\emph{whether}, and
\emph{because} in a sentence.  In set theory, everything is a set and all equations $a \eq b$ are propositions; our definition of $a \eq b$ is
designed to make the transition from set theory to type theory minimally disconcerting.

(Good motivation for the form of the equal sign in the notation $a=b$ is provided by a remark made by Robert Recorde in 1557 in the \emph{Whetstone of Witte}\footcite{WhetstoneOfWitte}:
``And to avoid the tedious repetition of these words \emph{is equal to}, I will set,
as I do often in work use, a pair of parallels, or twin lines of one length, thus: $=$,
because no two things can be more equal.''\footnote{\textfrak{%
    And to auoide the tediouse repetition of these woordes : is equalle to :
    I will sette as I doe often in woorke vse, a paire of paralleles,
    or Gemowe lines of one lengthe, thus{}:%
    $\begin{tikzcd}[cramped,ampersand replacement=\&]
      {}\ar[r,equal]\&{}\end{tikzcd}$,
    bicause noe .2. thynges, can be moare equalle.}}
In fact, the remark of Recorde presages the approach described in this book, for although those two little lines are congruent,
they were not considered to be equal traditionally, since they are in different places, whereas they may be considered to be equal in the presence of univalence,
which converts congruences to identifications.)
%% Robert Recorde, The Whetstone of Witte (London, England: John Kyngstone, 1557), p. 236
%% https://archive.org/stream/TheWhetstoneOfWitte#page/n237/mode/2up

Let $X$ be a type.
If for any $x:X$ and any $y:X$ the identity type $x \eqto y$ is a set,
then we shall say that $X$ is a \emph{groupoid},\index{groupoid}
also called a $1$-\emph{type}.

The pattern continues.  If for any $n:\NN$, any $x:X$, and any $y:X$
the identity type $x \eqto y$ is an $n$-\emph{type},\index{type!$n$-truncated}
then we shall say that $X$ is an $(n+1)$-\emph{type}.
If $X$ is an $n$-type, we also say that $X$ is \emph{$n$-truncated}.

We prove that every proposition is a set, from which it follows
by induction that every $n$-type is an $(n+1)$-\emph{type}.

\begin{lemma}\label{lem:prop-is-set}
Every type that is a proposition is also a set.
\end{lemma}
\begin{proof}
Let $X$ be a type and let $f: \prod_{a,b:X} (a \eqto b)$. Let $a,b,c : X$ and
let $P(x)$ be the type $a \eqto x$ depending on $x:X$. Then
$f(a,b):P(b)$ and $f(a,c):P(c)$. By path induction we construct for
all $q:b \eqto c$ an identification of type $q\cdot f(a,b) \eqto f(a,c)$.
For this it suffices to observe that $\refl{b} \cdot f(a,b)$ and
$f(a,b)$ are equal by definition. Since $a$ is arbitrary,
it follows that any $q:b \eqto c$ can be identified with
$f(b,c)\cdot f(b,b)^{-1}$, which doesn't depend on $q$.
Hence $X$ is a set.
\end{proof}

A more interesting example of a set is $\bool$.

\begin{lemma}\label{lem:isset-bool}
$\bool$ is a set.
\end{lemma}
\begin{proof}
The following elegant, self-contained proof is due to Simon Huber.
For proving $p \eqto q$ for all $b,b':\bool$ and $p,q: b \eqto b'$,
it suffices (by induction on $q$) to show
$p \eqto \refl{b}$ for all $b:\bool$ and $p: b \eqto b$.
To this end, define by induction on $b,b':\bool$,
a type $C(b,b',p)$ for all $p: b \eqto b'$, by setting
$C(\yes,\yes,p)\defeq (p \eqto \refl{\yes})$,
$C(\no,\no,p)\defeq (p \eqto \refl{\no})$,
and arbitrary in the other two cases.
By induction on $b$ one proves that $C(b,b,p) \eqto (p \eqto \refl{b})$ for all $p$.
Hence it suffices to prove $C(b,b',p)$ for all $b,b':\bool$
and $p: b \eqto b'$. By induction on $p$ this reduces to
$C(b,b,\refl{b})$, which is immediate by induction on $b:\bool$.
\end{proof}

We now collect a number of useful results on propositions.

\begin{lemma}\label{lem:prop-utils}
Let $A$ be a type, and let $P$ and $Q$ propositions.
Let $R(a)$ be a proposition depending on $a:A$. Then we have:
\begin{enumerate}
\item\label{prop-utils-false-true} $\false$ and $\true$ are propositions;
\item\label{prop-utils-codom} $A\to P$ is a proposition;
\item\label{prop-utils-pi} $\prod_{a:A} R(a)$ is a proposition;
\item\label{prop-utils-times} $P\times Q$ is a proposition;
\item\label{prop-utils-sum} if $A$ is a proposition, then $\sum_{a:A} R(a)$ is a proposition;
%\item\label{prop-utils-eq} $P \equivto Q$ is a proposition;
\item\label{prop-utils-lem} $P \amalg \neg P$ is a proposition.
\end{enumerate}
\end{lemma}

\begin{proof}
\ref{prop-utils-false-true}:
If $p,q : \false$, then $p \eqto q$ holds by induction for $\false$.
If $p,q : \true$, then $p \eqto q$ is proved by double induction,
which reduces the proof to observing that $\refl{\triv}: \triv \eqto \triv$.

\ref{prop-utils-codom}:
If $p,q : A\to P$, then $p \eqto q$ is proved by first observing that $p$ and $q$
are functions which, by function extensionality, can be identified if they have
equal values $p(x) = q(x)$ in $P$ for all $x$ in $A$. This is
actually the case since $P$ is a proposition.

\ref{prop-utils-pi}:
If $p,q : \prod_{a:A} R(a)$ one can use the same argument as for $A\to P$
but now with \emph{dependent} functions $p,q$.

\ref{prop-utils-times}:
If $(p_1,q_1),(p_2,q_2) : P\times Q$, then $(p_1,q_1) \eqto (p_2,q_2)$
is proved componentwise.  Alternatively, we may regard this case as a special case of \ref{prop-utils-sum}.

\ref{prop-utils-sum}:
Given $(a_1,r_1), (a_2,r_2) : \sum_a R(a)$, we must establish that $(a_1,r_1) \eqto (a_2,r_2)$.  Combining the map in \cref{def:pairtopath} with the
identity type in \cref{def:pathover-trp} yields a map $ \left( \sum_{u : a_1 = a_2} \trp[Y]{u}(r_1) = r_2 \right) \to \left( (a_1,r_1) \eqto (a_2,r_2)
\right)$, so it suffices to construct an element in the source of the map.  Since $A$ is a proposition, we may find $u : a_1 = a_2$.  Since
$R(a_2)$ is a proposition, we may find $v : \trp[Y]{u}(r_1) = r_2$.  The pair $(u,v)$ is what we wanted to find.

\ref{prop-utils-lem}:
If $p,q : P\amalg \neg P$, then we can distinguish four cases
based on $\inl{}/\inr{}$, see \cref{sec:sum-types}. In two cases
we have both $P$ and $\neg P$ and we are done. In the other two,
either $p\jdeq \inl{p'}$ and $q\jdeq \inl{q'}$ with $p',q':P$,
or $p\jdeq \inr{p'}$ and $q\jdeq \inr{q'}$ with $p',q':\neg P$.
In both these cases we are done since $P$ and $\neg P$
are propositions.
\end{proof}

Several remarks can be made here. First, the lemma supports the
use of $\false$ and $\true$ as truth values, and the use of
$\to,\prod,\times$ for implication, universal quantification,
and conjunction, respectively. Since $\false$ is a proposition,
it follows by \ref{prop-utils-codom} above that
$A\to\emptytype$ is a proposition for any type $A$.
As noted before, \ref{prop-utils-codom} is a
special case of \ref{prop-utils-pi}.

Notably absent in the lemma above are disjunction
and existential quantification. This has a simple reason:
$\true\amalg \true$ has two distinct elements
$\inl{\triv}$ and $\inr{\triv}$, an is therefore \emph{not} a proposition.
Similarly, $\sum_{n:\NN} \true$ has infinitely many
distinct elements $(n,\triv)$ and is not a proposition. We will explain
in \cref{sec:prop-trunc} how to work with disjunction and
existential quantification for propositions.

The lemma above has a generalization from propositions to
$n$-types which we state without proving.
(The proof goes by induction on $n$, with the lemma above serving as the base case where $n$ is $-1$.)

\begin{lemma}\label{lem:level-n-utils}
Let $A$ be a type, and let $X$ and $Y$ be $n$-types.
Let $Z(a)$ be an $n$-type depending on $a:A$. Then we have:

\begin{enumerate}
\item\label{level-n-utils-codom} $A\to X$ is an $n$-type;
\item\label{level-n-utils-pi} $\prod_{a:A} Z(a)$ is an $n$-type;
\item\label{level-n-utils-times} $X\times Y$ is an $n$-type.
\item\label{level-n-utils-sum} if $A$ is an $n$-type, then $\sum_{a:A} Z(a)$ is an $n$-type;
\end{enumerate}
\end{lemma}

We formalize the definitions from the start of this section.
\begin{definition}\label{def:isSet}
\begin{align*}
\isprop(P) &\defeq\prod\nolimits_{p,q:P}(p \eqto q)\\
\isset(S) &\defeq\prod\nolimits_{x,y:S}\isprop(x \eqto y)\jdeq
                  \prod\nolimits_{x,y:S}\prod\nolimits_{p,q:(x \eqto y)}(p \eqto q)\\
\isgrpd(G) &\defeq\prod\nolimits_{g,h:G}\isset(g \eqto h)\jdeq \ldots\qedhere
\end{align*}
\end{definition}
\begin{lemma}\label{lem:isX-is-prop}
  For any type $A$, the following types are propositions:
  \begin{enumerate}
    \item $\iscontr(A)$;
    \item $\isprop(A)$;
    \item $\isset(A)$;
    \item $\isgrpd(A)$;
    \item the type that encodes whether $A$ is an $n$-type, for $n \ge 0$.
  \end{enumerate}
\end{lemma}

Consistent with that, we will use identifiers starting with ``is'' only for names of types
that are propositions. Examples are $\isset(A)$ and $\isgrpd(A)$,
and also $\isEq(f)$.

\begin{proof}
Recall that $\iscontr(A)$ is $\sum_{a:A} \prod_{y:A} (a \eqto y)$.
Let $(a,f)$ and $(b,g)$ be elements of the type $\iscontr(A)$.
By \cref{def:pairtopath}, to give an element of $(a,f) \eqto (b,g)$ it suffices
to give an $e : a \eqto b$ and an $e' : \pathover{f}{x\mapsto\prod_{y:A} (x \eqto y)}{e}{g}$.
For $e$ we can take $f(b)$; for $e'$ it suffices by \cref{def:pathover-trp}
to give an $e'' : \trp e f \eqto g$. Clearly, $A$ is a proposition and hence
a set by \cref{lem:prop-is-set}. Hence the type of $g$ is a proposition
by \cref{lem:prop-utils}\ref{prop-utils-pi}, which gives us $e''$.

We leave the other cases as exercises.
\end{proof}

\begin{xca}\label{xca:isX-is-prop}
Make sure you understand that $\isprop(P)$ is a proposition,
using the same lemmas as for $\iscontr(A)$.
Show that $\isset(S)$, $\isgrpd(G)$ and $\isEq(f)$ are propositions.
\end{xca}

The following exercise shows that the inductive definition of $n$-types can
indeed start with $n$ as $-2$, where we have the contractible types.

\begin{xca}\label{xca:prop-contractible=}
Given a type $P$, show that $P$ is a proposition if and only if $p \eqto q$ is contractible,
for any $p, q: P$.
\end{xca}

\begin{remark}\label{rem:diagram}
We now present the notion of a \emph{diagram}\index{diagram}.  A diagram is a graph
whose vertices are types and whose edges are functions.  Here is an example.
\[
\begin{tikzcd}
  X \ar[r,"f"] \ar[d,"p"] & Y \ar[d,"q"] \\
  S \ar[r,"g"]            & T
\end{tikzcd}
\]
The information conveyed by this diagram to the reader is that $X$, $Y$, $S$, and $T$ are types, and that $f$, $g$, $p$, and $q$
are functions; moreover, $f$ is of type $X \to Y$, $g$ is of type $S \to T$, $p$ is of type $X \to S$, and $q$ is of type $Y \to T$.

Observe that we can travel through the diagram from $X$ to $T$ by following first the arrow labeled $f$ and then the arrow labelled $q$.
Consequently, the composite function $q \circ f$ is of type $X \to T$.

There is another route from $X$ to $T$ : we could follow first the arrow labeled $p$ and then the arrow labelled $g$.
Consequently, the composite function $g \circ p$ is also of type $X \to T$.

We say that a diagram \emph{is commutative by definition}\index{diagram!commutative by definition} if, whenever there are two routes from one
vertex to another, the corresponding composite functions are equal by definition.  For example, in the diagram above, the condition would be that
$g \circ p \jdeq q \circ f$.

When the function type from any vertex of a diagram to any other vertex of the diagram is a set, then equality of functions is a proposition,
and we may consider whether two functions are equal.  In that case, we say that a diagram \emph{is commutative}\index{diagram!commutative} if,
whenever there are two routes from one vertex to another, the corresponding composite functions are equal.  For example, in the diagram above,
the condition would be that $g \circ p \eq q \circ f$.

In general, a diagram is a visual way to represent identity types.
For example, if in the above diagram the type $X\to T$ is not
a set, then the diagram represents the identity type
$g \circ p \eqto q \circ f$.


There are other sorts of diagrams.  For example, identifications may be composed, and thus we may have a diagram of identifications between
elements of the same type.  For example, suppose $W$ is a type, suppose that $x$, $y$, $s$, and $t$ are elements of $W$, and consider
the following diagram.
\[
\begin{tikzcd}
  x \ar[r,eqr,"f"] \ar[d,eqr,"p"] & y \ar[d,eqr,"q"] \\
  s \ar[r,eqr,"g"]                & t
\end{tikzcd}
\]
It indicates that $f$ is of type $x \eqto y$, $g$ is of type $s \eqto t$,
$p$ is of type $x \eqto s$, and $q$ is of type $y \eqto t$.  We may
also consider whether such a diagram is commutative by definition, or,
in the case where all the identity types are sets, is commutative.
Such diagrams are again a visual way to represent identity types.
\footnote{When diagrams get more complicated, the information
they convey is not always sufficient to find out which identity
type(s) they represent. In such cases additional information will
be provided.}%
For example, the above diagram represents the identity type
$g \circ p \eqto q \circ f$. For a concrete example, see
the naturality square in \cref{def:naturality-square}.
\end{remark}

\section{Propositional truncation and logic}
\label{sec:prop-trunc}

As explained in \cref{sec:props-sets-grpds},
the type formers $\to,\prod,\times$
can be used with types that are propositions for the logical operations of implication,
universal quantification, and conjunction, respectively.
Moreover, $\true$ and $\false$ can be used as truth values,
and $\neg$ can be used for negation.
We have also seen that ${\amalg}$ and $\Sigma$ can lead to types
that are not propositions, even though the constituents are
propositions. This means we are still lacking disjunction ($P \vee Q$) and existence ($\exists_{x:X} P(x)$)
from the standard repertoire of logic, as well as the notion of \emph{non-emptiness} of a type.
In this section we explain how to implement these three notions.

To motivate the construction that follows, consider non-emptiness of a type $T$.  In order to be in a position to encode the mathematical
assertion expressed by the English phrase ``$T$ is non-empty'', we will need a proposition $P$.  The proposition $P$ will have to be constructed
somehow from $T$.  Any element of $T$ should somehow give rise to an element of $P$, but, since all elements of propositions are equal to each
other, all elements of $P$ arising from elements of $T$ should somehow be made to equal each other.  Finally, any proposition $Q$ that is a
consequence of having an element of $T$ should also be a consequence of $P$.

We define now an operation called propositional truncation,\footnote{%
The name ``truncation'' is slightly misleading since it suggests leaving
something out, whereas the correct intuition is one of adding identifications
so everything becomes equal.}
that enforces that all elements of a type become equal.

\begin{definition}\label{def:prop-trunc}
Let $T$ be a type. The \emph{propositional truncation} of $T$
is the type  $\Trunc{T}$ defined by the following constructors:%
\index{type!propositional truncation}\index{propositional truncation}%
\index{truncation!propositional}%
\glossary(1truncType){$\protect\Trunc{T}$}{propositional truncation of a type $T$}
\begin{enumerate}
\item an \emph{element} constructor $\trunc{t} : \Trunc{T}$ for all $t:T$;%
  \glossary(1trunc){$\protect\trunc{t}$}{constructor for the propositional truncation $\Trunc{T}$ applied to $t:T$}
\item an \emph{identification} constructor providing an identification of type $x \eqto y$  for all $x,y:\Trunc{T}$.
\end{enumerate}
The identification constructor ensures that $\Trunc{T}$ is a
proposition. The induction principle states that,
for any family of propositions $P(x)$ parametrized by a variable $x:\Trunc{T}$,
in order to prove $\prod_{x:\Trunc{T}} P(x)$,
it suffices to prove $\prod_{t:T} P(\trunc{t})$. In other
words, in order to define a function $f:\prod_{x:\Trunc{T}} P(x)$,
it suffices to give a function $g: \prod_{t:T} P(\trunc{t})$.
Moreover, the function $f$ will satisfy $f(\trunc{t})\jdeq g(t)$ for all $t:T$.
\end{definition}

Consider the special case where the family $P(x)$ is constant.
We see that any function $g: T\to P$ to a proposition $P$ yields a (unique) function $f:\Trunc{T}\to P$
satisfying $f(\trunc{t})\jdeq g(t)$ for all $t:T$.\footnote{%
Given $t, t' : T$, we have an identification of type $ \trunc t \eqto \trunc {t'} $.
The existence of the function $g$ implies that we have an identification of type $ g(\trunc t) \eqto g(\trunc {t'}) $,
and hence an identification of type $f(t) \eqto f(t')$.  Thus a necessary condition for the existence of $g$ is
the existence of identifications of type $f(t) \eqto f(t')$.  That justifies the
the hypothesis that $P$ is proposition.}
A useful consequence of this recursion principle is that,
for any proposition $P$, precomposition with $\trunc{\_}$ is an equivalence of type
\[
(\Trunc{T} \to P) \quad \equivto \quad (T \to P).
\]
This is called \emph{the universal property of propositional truncation}.

\begin{definition}\label{def:non-empty}
  Let $T$ be a type.
  We call $T$ \emph{non-empty}
  if we have an element of $\Trunc{T}$.\footnote{%
    We may alternatively say that $T$ is \emph{inhabited},
    in order to avoid confusion with the
    concept of $T$ \emph{not being empty},
    which would be represented by the proposition
    $\neg(T \eqto \emptytype)$, which is equivalent to
    $\neg\neg T$.}
\end{definition}

When we view propositional truncation as an operation on types,
the type of $\Trunc \blank$ is $\UU\to\UU$. However, that view
does not take into account that $\Trunc T$ is a proposition.
It is more informative
to pack this information into the codomain of the operation
and let $\Trunc \blank$ have the type $\UU\to\sum_{X:\UU}\isprop(X)$.
The type $\sum_{X:\UU}\isprop(X)$ is also denoted as $\Prop_\UU$
and even as $\Prop$. See \cref{def:Prop-Set} for more information.

Now that propositional truncation is available,
we are ready to define logical disjunction and existence.

\begin{definition}
  Given propositions $P$ and $Q$, define their \emph{disjunction}
  by  $(P \vee Q) \defeq \Trunc{P \amalg Q}$.%
  \index{disjunction}\glossary(2vee){$\vee$}{disjunction of propositions}
  It expresses the property that $P$ is true or $Q$ is true.
\end{definition}

\begin{definition}
  Given a type $X$ and a family $P(x)$ of propositions parametrized by a variable $x$ of type $X$,
  define a proposition that encodes the property that there exists a member of the family for which
  the property is true by $(\exists_{x:X} P(x)) \defeq \Trunc*{\sum_{x:X} P(x)}.$%
  \index{exists}\glossary(2exists){$\protect\exists_{x:X}P(x)$}{proposition expressing
    existential quantification}
  It expresses the property that there \emph{exists} an element $x:X$ for which the property $P(x)$ is true; the element $x$ is not
  given explicitly.
\end{definition}

The following logical quantifier could have been defined earlier, since it doesn't use propositional truncation.  We present
it now, for completeness.

\begin{definition}
  Given a type $X$ and a family $P(x)$ of propositions parametrized by a variable $x$ of type $X$,
  define a proposition that encodes the property that there exists a \emph{unique} member of the family for which
  the property is true by the proposition $(\existsuniq_{x:X} P(x)) \defeq \iscontr({\sum_{x:X} P(x)})$.
\end{definition}

\begin{xca}
  Given $x:\Trunc{T}$, prove that $\exists_{t:T} ( x \eq \trunc t )$.
\end{xca}

\begin{xca}\label{xca:prop-trivia-1}
  Suppose $P$ is a proposition.  Produce an equivalence of type $P \equivto \Trunc P$.
\end{xca}

The exercise above us to easily convert elements of type $\Trunc P$ to elements of type
$P$ when $P$ is a proposition.

\begin{definition}\label{def:connected}
  Let $A$ be a type. For any element $a$ of $A$, the type
   $A_{(a)}\defeq \sum_{x:A} \Trunc { a \eqto x } $
  is called the \emph{connected component} of $a$ in $A$.\footnote{%
  In \cref{sec:subtype} we will define the notion of subtype.
  It will turn out that $A_{(a)}$ is a subtype of $A$.}
  We say that elements $x,y$ of $A$ are \emph{in the same component}
  of $A$ if $\Trunc { x \eqto y }$. % for then $A_{(x)} = A_{(y)}$.
  The type $A$ is called \emph{connected}\footnote{%
    In \cref{xca:sum-of-conn-components} below we will
    define the \emph{set of connected components} of a type.}
  if it is non-empty with
  all elements in the same component.  Formally, this property is encoded by the following proposition.
  \[
    \isconn(A) \defeq \Trunc{A} \times \prod_{x,y:A} \Trunc { x \eqto y }.\qedhere
  \]
\end{definition}

Note that the empty type $\emptytype$ is \emph{not} connected.

One can view being connected as a weak form
of being contractible -- without direct access to a center and to
identifications of elements.

\begin{xca}\label{xca:component-connected}
  Show that the component of $a$ in $A$ is connected.
  Show that elements in the same component have the same
  \emph{propositional} properties, that is,
  for any $P:A\to\Prop$, $P(x)\eqto P(y)$
  for any $x,y:A$ with $\Trunc {x=y}$.
\end{xca}

\begin{xca}\label{xca:connected-trivia-2}
  Show that any connected set is contractible.
\end{xca}

\begin{xca}\label{xca:connected-trivia}
Let $A$ be a connected type, and suppose that $a \eqto a$ is a proposition for every $a:A$.
Show that $A$ is contractible.
\end{xca}

\begin{xca}\label{xca:connected-trivia-1}
  Show that $\sum_{x:A}B(x)$ is connected when $A$ is connected
  and $B(x)$ is connected for any $x:A$.
\end{xca}

In the following definition we introduce the adverb \emph{merely}, which serves as a quicker way to say \emph{the propositional truncation of}
in English speech.

\begin{definition}\label{def:merely}\index{merely}
  What we mean by \emph{merely} constructing an element of a type $T$ is constructing an element of $\Trunc T$.
\end{definition}

For example, a type is non-empty if it \emph{merely has an element}, and a type is connected if any two elements can be
\emph{merely identified} with each other.


\section{More on equivalences; surjections and injections}
\label{sec:more-on-equivalences}

In this section we collect a number of useful results on equivalences.

Consider the function $f:\bn{1}\to\bn{2}$ that is constant $0$.
The fibers of $f$ at $0$ and $1$ are $\sum_{x:\bn{1}} 0\eqto 0$
and $\sum_{x:\bn{1}} 1\eqto 0$, respectively.
The latter fiber is not contractible: having an element
of it would mean having an element of $1\eqto 0$,
which would in turn lead to an element in $\false$
(using a similar reasoning as in \cref{sec:finite-types}).
Hence $f$ is not an equivalence.
Observe that both fibers are propositions,
that is, contain at most one element.

As a function between sets
$f$ is an injection (one-to-one), but not a surjection.
We need these important concepts for types in general.
We define them as close as possible to their
usual meaning in set theory: a function from $A$ to $B$ is
surjective if the preimage of any $b:B$ is non-empty,
and injective if such preimages contain at most one element.
This motivates the following definitions.

\begin{definition}\label{def:surjection}
A function $f:A\to B$ is a \emph{surjection}, or is \emph{surjective},
if for all $b:B$ there exists an $a:A$ such that $b \eqto f(a)$,
that is, $\exists_{a:A} (b \eqto f(a))$.\footnote{%
  A function $f:A\to B$ is a \emph{split surjection}
  if for all $b:B$ we have an $a:A$ with $b \eqto f(a)$,
  in other words, we have a function of type
  $\prod_{b:B} \sum_{a:A} (b \eqto f(a))$.
  This is equivalent to saying we have a function
  $g:B\to A$ and an identification $p: f\circ g \eqto \id_B$
  (such a $g$ is called a \emph{section} of $f$).}
\end{definition}

\begin{definition}\label{def:injection}
  A function $f:A\to B$ is an \emph{injection}\index{injection}, or is \emph{injective}\index{injective},
  if $f^{-1}(b)$ is a proposition for all $b:B$.  The property of being an injection is encoded by
  the type $\isinj(f) \defeq \prod_{b:B} \isprop(\inv f (b))$.
\end{definition}

\begin{xca}\label{xca:inj-sets}
  Show that if $A,B$ are sets, then a function
  $f : A \to B$ is injective if and only if
  $f(a) \eqto f(a')$ implies $a \eqto a'$ for all $a,a'$.
\end{xca}

\begin{lemma}\label{lem:inj+surj}
For all types $A,B$, a function $f: A\to B$ is an equivalence
if and only if $f$ is an injection and a surjection.
\end{lemma}

\begin{proof}
If $f: A\to B$ is an equivalence, then all fibers are contractible,
so $f$ is both an injection and a surjection. Conversely,
if $f$ is both injective and surjective, we show that
$f^{-1}(b)$ is contractible, for each $b:B$.
Being contractible is a proposition, so by \cref{def:prop-trunc}
we can drop the truncation in $\Trunc{\sum_{a:A} b \eqto f(a)}$.
Now apply injectivity.\footnote{%
  This argument applies generally:
  Any non-empty proposition is contractible.}
\end{proof}

If the types $A$ and $B$ in the above lemma are \emph{sets},
then we call equivalences between $A$ and $B$ also \emph{bijections}.

\begin{corollary}\label{cor:inj+connected}
Let $A,B$ be types such that $A$ is non-empty and $B$ is connected.
Then any injection $f: A\to B$ is an equivalence.
\end{corollary}
\begin{proof}
By \cref{lem:inj+surj} it suffices to show that $f$ is surjective.
This is a proposition, so by \cref{def:prop-trunc} and $\Trunc{A}$
we may assume $a:A$, so $f(a):B$. By $\prod_{x,y:B} \Trunc{x \eqto y}$
we now get that all preimages under $f$ are non-empty.
\end{proof}

\begin{lemma}\label{lem:whenisbasespaceconnected}
Let $f:X\to Y$ be a surjective map from a connected type $X$. Then $Y$ is connected too.
\end{lemma}
\begin{proof}
For any map $f:X\to Y$ between arbitrary types, if $y,y':Y$ and we are given
$x,x':X$, $p:y \eqto f(x)$, $p':y' \eqto f(x')$ and $q:x \eqto x'$,
then we have a path between $y$ and $y'$ given by the composite
\[
  \begin{tikzcd}
    y \ar[r,"=","p"'] & f(x) \ar[r,"=","f(q)"'] & f(x') \ar[r,"=","\inv{p'}"'] & y'.
  \end{tikzcd}
\]
Now the lemma follows by eliminating the propositional truncations in the assumptions,
using that the conclusion is a proposition.
\end{proof}

\begin{construction}\label{con:fib-vs-path}
  For every $f:A\to B$, $b:B$, and $z,z' : f^{-1}(b)$,
  there is an equivalence
  \begin{equation}\label{eq:fib_vs-path}
    (z \eqto z') \equivto \ap{f}^{-1}(\snd{z'} \cdot \inv{\snd{z}}).
  \end{equation}
\end{construction}

\begin{implementation}{con:fib-vs-path}
  We can construct this equivalence for $z\jdeq(a,p)$ and $z'\jdeq(a',p')$,
  where $a,a':A$, $p:b \eqto f(a)$ and $p':b \eqto f(a')$,
  as the composition\marginnote{%
    \noindent\normalsize\begin{tikzpicture}
      \node (X) at (0,-1.5) {$B$};
      \draw (0,-1)
      .. controls ++(170:-1) and ++(180:1) .. (2,-1.8)
      .. controls ++(180:-1) and ++(270:1.5) .. (3.5,0.5)
      .. controls ++(270:-1.5) and ++(80:1.4)  .. (-1,1)
      .. controls ++(80:-1.4)  and ++(170:1) .. (0,-1);
      \node[dot,label=left:$f(a)$] (a) at (0,0) {};
      \node[dot,label=below:$b$] (b) at (1.8,-1) {};
      \node[dot,label=right:$f(a')$] (c) at (2.3,.6) {};
      \node (ct) at (1.2,1) {$\ap{f}(q)$};
      \draw[<-] (a) .. controls ++(-20:1) and ++(170:1) .. node[auto,swap] {$p$} (b);
      \draw[->] (b) .. controls ++(10:1) and ++(-70:1) .. node[auto,swap] {$p'$} (c);
      \draw[->] (a) .. controls ++(45:1) and ++(170:1) .. (c);
    \end{tikzpicture}}
  \begin{align*}
    (z \eqto z')
    &\jdeq \bigl( (a,p) \eqto (a',p') \bigr) \\
    &\equivto \sum_{q : a \eqto a'} \pathover{p}{b \eqto f(\blank)}{q}{p'} \\
    &\equivto \sum_{q : a \eqto a'} \ap{f}(q) \cdot p \eqto p' \\
    &\equivto \sum_{q : a \eqto a'} p' \cdot \inv p \eqto \ap{f}(q) \\
    &\jdeq \ap{f}^{-1}(p' \cdot \inv p).
  \end{align*}
  The second equivalence relies on \cref{def:pathover-trp}
  and \cref{lem:trp-in-fx=Ygx}.
\end{implementation}

\begin{lemma}\label{lem:inj-ap}
  A function $f:A\to B$ is an injection if and only if
  each induced function
  $\ap{f}: (a \eqto a') \to (f(a) \eqto f(a'))$ is an equivalence,
  for all $a,a':A$.\footnote{%
    \emph{Warning:}
    If $A$ and $B$ are sets, then each $\ap{f}$ is an equivalence
    if and only if all implications $(f(a) \eqto f(a')) \to (a \eqto a')$
    hold, but this is in general not sufficient.}
\end{lemma}

\begin{proof}
  It follows directly from \eqref{eq:fib_vs-path}
  that if $\ap{f}$ is an equivalence,
  then $f^{-1}(b)$ is a proposition,
  as all its identity types (fibers of $\ap{f}$) are contractible.

  On the other hand, if we fix $a,a':A$ and $p:f(a) \eqto f(a')$,
  then \eqref{eq:fib_vs-path} applied to $b \defeq f(a)$,
  $z \defeq (a,\refl{f(a)})$ and
  $z' \defeq (a',p)$,
  gives $\ap{f}^{-1}(p) \equivto (z \eqto z')$,
  which shows that if each $f^{-1}(b)$ is a proposition,
  then $\ap{f}$ is an equivalence.
\end{proof}


\begin{corollary}\label{cor:fib-vs-path}
Let $A$ and $B$ be types and let $f:A\to B$ be a function. Then we have:
\begin{enumerate}
\item\label{set-fib-vs-path}
All fibers of $f$ are $(n{+}1)$-types if and only if all fibers of
each map induced by $f$ on identity types are $n$-types;
\item\label{set-fib-vs-path-point}
If $A$ is connected and $a:A$, then
all fibers of $f$ are $(n{+}1)$-types if and only if all fibers of
$\ap{f}: (a \eqto a) \to (f(a) \eqto f(a))$ are $n$-types;
\item\label{conn-fib-vs-path}
If $A$ and $B$ are connected, then $f$ is an equivalence
if and only if each map induced by $f$ on identity types is an equivalence;
\item\label{conn-fib-vs-path-point}
If $A$ and $B$ are connected and $a:A$, then $f$ is an equivalence
if and only if $\ap{f}: (a \eqto a) \to (f(a) \eqto f(a))$ is an equivalence.
\end{enumerate}
\end{corollary}
\begin{proof}
\ref{set-fib-vs-path} When $n$ is $-2$ this is \cref{lem:inj-ap}
and the proof for $n\geq -1$ is similar.
\ref{set-fib-vs-path-point} By \ref{set-fib-vs-path} and \cref{xca:component-connected}.
\ref{conn-fib-vs-path} By \cref{lem:inj-ap} and \cref{cor:inj+connected}.
\ref{conn-fib-vs-path-point} By \ref{conn-fib-vs-path} and \cref{xca:component-connected}.
\end{proof}

\begin{xca}\label{xca:sum-equivalences}
Let $A,B:\UU$, $F:A\to\UU$ and $G:B\to\UU$,
and $f: A\equivto B$ and $g:\prod_{a:A}(F(a) \equivto G(f(a)))$.
Give an equivalence from $\sum_{a:A} F(a)$ to $\sum_{b:B} G(b)$.
(An important special case is $F\jdeq G\circ f$.)
\end{xca}

Another application of propositional truncation
is the notion of image.
\begin{definition}\label{def:prop-image}
  Let $A,B$ be types and let $f : A \to B$. We define the \emph{image} of $f$ as
  \glossary(ima){$\protect\im(f)$}{the (propositional) image of $\protect f$}
  \[
    \im(f) \defeq \sum_{y:B}\exists_{x:A}(y \eqto f\,x).\qedhere
  \]
\end{definition}

Note that $(\exists_{x:A}(y \eqto f\,x)) \jdeq \Trunc{f^{-1}(y)}$,
the propositional truncation of the fiber.
For this reason, $\im(f)$ is called the \emph{propositional} image.
Later we will meet other notions of image, based on other truncation operations.

\begin{xca}\label{xca:unique-fact-image}
  Show that the image of $f : A \to B$ induces a factorization
  $f \eqto i\circ p$, visualized by the following diagram\footnote{%
  This diagram actually commutes by definition.}
  \[
    \begin{tikzcd}
      A \ar[rr,"f"]\ar[dr,"p"'] & & B \\
      & \im(f)\ar[ur,"i"'] &
    \end{tikzcd}
  \]

  where $p$ is surjective and $i$ is injective. Show that the
  following type of image factorizations of $f : A \to B$~\marginnote{%
  Thus the image factorization of $f$ is a 6-tuple. For convenience
  we may simplify and speak of the "image factorization $f \eqto h\circ g$."
  Here $C$ is implicit in the types of $g$ and $h$. The particular
  identification of $f$ with $h\circ g$ follows from the context,
  as do the proofs that $g$ is an injection and $h$ is a surjection.}
  is contractible:
  \[
  \sum_{C:\UU}\sum_{g:A\to C}\sum_{h: C\to B}
  ((f \eqto h\circ g) \times \issurj(g) \times \isinj(h)).\qedhere
  \]
\end{xca}

\begin{xca}\label{xca:prop-image-is-set}
Let $A$ be a type and $B$ as set and $f:A\to B$.
Show that $\im(f)$ is a set.
\end{xca}

\begin{xca}\label{xca:all-prop-image}
Let $f:A\to B$ for $A$ and $B$ types, and let $P(b)$ be a proposition
depending on $b:B$.
Show that $\prod_{z:\im(f)} P(\fst(z))$ if and only if $\prod_{a:A} P(f(a))$.
%(Hint: for the if-direction, use truncation elimination and path induction.)
\end{xca}



\section{Decidability, excluded middle and propositional resizing}
\label{sec:decidability}

Recall from \cref{lem:prop-utils}\ref{prop-utils-lem} that $P\amalg \neg P$ is a proposition whenever $P$ is a proposition.
\begin{definition}\label{def:decidability}
  A proposition $P$ is called \emph{decidable}
  if $P\amalg\neg P$ holds.\index{decidable proposition}
\end{definition}
In traditional mathematics, it is usually assumed that
every proposition is decidable.
This is expressed by the following principle, commonly abbreviated LEM.
\begin{principle}[Law of Excluded Middle]
  \label{pri:lem}\index{Law of Excluded Middle}\index{LEM|see{Law of Excluded Middle}}%
  For every proposition $P$, the proposition $P \amalg \neg P$ holds.
\end{principle}

(The ``middle'' ground excluded by this principle is the possibility that there
is a proposition that is neither true nor false.)

Type theory is born
in a constructivist tradition
which aims at developing as much mathematics as
possible without assuming the Law of Excluded Middle.\footnote{%
  Besides any philosophical reasons,
  there are several pragmatic reasons
  for developing constructive mathematics.
  One is that proofs in constructive mathematics
  can be executed as programs,
  and another is that the results also hold in non-standard models,
  for instance a model where every type has a topological structure,
  and all constructions are continuous.
  See also \cref{ft:cohesive}.}
Following this idea, we will
explicitly state whenever we are assuming the Law of Excluded Middle.
\begin{xca}\label{xca:lem-prop}
  Show that the Law of Excluded Middle is equivalent to asserting
  that the map $(\yes \eq \blank) : \bool \to \Prop$
  is an equivalence.
\end{xca}
A useful consequence of the Law of Excluded Middle is the principle of
``proof by contradiction'': to prove a proposition $P$,
assume its negation $\neg P$ and derive a contradiction.
Without the Law of Excluded Middle, this proves only the double negation of
$P$, that is $\neg \neg P$.  However, with the Law of Excluded Middle,
one can derive $P$ from the latter: indeed, according to the
Law of Excluded Middle, either $P$ or $\neg P$ holds;
but $\neg P$ leads to a contradiction by hypothesis, making $P$ hold
necessarily.

%\begin{xca}\label{xca:not-not-lemP}
%  Without using LEM, show that $((P\amalg (P\to \false))\to\false)\to\false$
%  for every proposition $P$.
%\end{xca}

\begin{xca}\label{xca:dne-lem}
  Show that, conversely, LEM follows from the principle of
  \emph{double-negation elimination}:
  For every proposition $P$, if $\neg \neg P$, then $P$ holds.
\end{xca}

\begin{remark}
  We will later encounter a weaker version of the Law of Excluded Middle, called the Limited
  Principle of Omniscience (\cref{LPO}), which is often enough.\footnote{%
    As the naming indicates, we can think of the Law of Excluded Middle itself as an omniscience
    principle, telling us for every proposition $P$,
    whether $P$ is true or false.
    It was this interpretation of the Law of Excluded Middle that led Brouwer to reject it
    in his 1908 paper on \emph{De onbetrouwbaarheid der logische
      principes}.\footnotemark{}}\footcitetext{Brouwer-1908}
\end{remark}

Sometimes we make use of the following,
which is another consequence of the Law of Excluded Middle:
\begin{principle}[Propositional Resizing]
  \label{pri:prop-resizing}\index{Propositional resizing}
  For any pair of nested universes $\UU:\UU'$, the map
  $(P\mapsto P):\Prop_\UU \to \Prop_{\UU'}$ is an equivalence.\footnote%
  {The map $P\mapsto P$ is welltyped by \emph{cumulativity}
  of the universes, that is, by point~\ref{it:cumulative}
  of \cref{sec:universes}. Note that the map is not
  the identity function due to its type.}
\end{principle}
\begin{xca}\label{xca:lem-prop-sizing}
  Show that if the Law of Excluded Middle holds,
  then Propositional Resizing holds.
\end{xca}


\section{The replacement principle}
\label{sec:replacement}

In this section we fix a universe $\UU$.
We think of types $A:\UU$ as \emph{small} compared to arbitrary types,
which are then \emph{large} in comparison.\footnote{%
  The terminology \emph{small}/\emph{large} is also known from set theory,
  where classes are large collections,
  and sets are small collections.}
Often we run into types that are not in $\UU$ (small) directly,
but are nevertheless equivalent to types in $\UU$.
\begin{definition}\label{def:ess-loc-small}
  We say that a type $A$ is \emph{essentially $\UU$-small} if we
  have a type $X:\UU$ and an equivalence $A \equivto
  X$. And $A$ is \emph{locally $\UU$-small} if all its identity types
  are essentially $\UU$-small.
\end{definition}
Note that $\sum_{X:\UU}(A \equivto X)$, the type expressing that
$A$ is essentially $\UU$-small, is a proposition by the
univalence axiom for $\UU$.
Of course, any $A:\UU$ is essentially $\UU$-small,
and any essentially $\UU$-small type is locally $\UU$-small.

To show that a type is locally $\UU$-small
we have to give a reflexive relation
$\mathrm{Eq}_A : A \to A \to \UU$
that induces, by path induction, a family of equivalences
$(x \eqto y) \equivto \mathrm{Eq}_A(x,y)$.

\begin{xca}
  Show that $\UU$ is locally $\UU$-small, and investigate
  the closure properties of essentially and locally $\UU$-small types.
  (For instance, show that if $A:\UU$ and $B(x)$ is a family of locally $\UU$-small
  types parametrized by $x:A$, then $\prod_{x:A}B(x)$ is locally $\UU$-small.)
\end{xca}

\begin{remark}
  Note that propositional resizing (\cref{pri:prop-resizing})
  equivalently says that any proposition is essentially $\UU$-small,
  where we may take $\UU$ to be the smallest universe $\UU_0$.
  When we assume this, we get that any set is locally $\UU_0$-small.
\end{remark}

We will make use of the following principle
(recall the definition of the image, \cref{def:prop-image}).
\begin{principle}[Replacement]
  \label{pri:replacement}\index{Replacement principle}
  For any map $f : A \to B$
  from an essentially $\UU$-small type $A$
  to a locally $\UU$-small type $B$,
  the image $\im(f)$ is essentially $\UU$-small.
\end{principle}
This is reminiscent of the replacement principle of set theory which states
that for a large (class-sized) function with domain a small set
and codomain the class $V$ of all small sets,
the image is again a small set.
This follows from our replacement principle,
assuming propositional resizing,
or the even stronger principle of the excluded middle.

The replacement principle can be proved using the join construction of the image, cf.~\citeauthor{Rijke-Join}\footcite{Rijke-Join},
which uses as an assumption that the universes
are closed under pushouts.\footnote{%
  Pushouts are certain higher inductive types that suffice
  to construct all the higher inductive types that we need,
  but we don't actually need them in this book.}
\begin{xca}\label{xca:comp-loc-small-ess-small}
  Show that the replacement principle implies that for any locally $\UU$-small type $A$,
  and any element $a:A$,
  the connected component $\conncomp A a$ is essentially $\UU$-small.
\end{xca}
Another consequence is that the type of finite sets, which we'll define below
in~\cref{def:groupoidFin}, is essentially small.


\section{Predicates and subtypes}
\label{sec:subtype}

In this section, we give two (equivalent) definitions of the notion
of a subtype of a given type $T$. The first definition is based
on the notion of a predicate on $T$. A predicate tells, or `predicates',
whether an element of $T$ belongs to the subtype. The second definition
is based on the notion of injection, defined in \cref{def:injection}.

\begin{definition}\label{def:predicate}
  Let $T$ be a type and let $P(t):\Prop$\footnote{%
    Recall that $\Prop$ abbreviates $\Prop_\UU \jdeq \sum_{T:\UU} \isprop(T)$.}
  be a family of propositions parametrized by a variable $t:T$.
  Then we call $P$ a \emph{predicate}\index{predicate} on $T$.\footnote{%
    Note that giving a predicate on $T$ is
    equivalent to giving a map $Q: T\to\Prop_\UU$
    for a suitable universe $\UU$, and we often say that $Q$ itself is the
    predicate. We leave $\UU$ implicit.}
  If $P(t)$ is a decidable proposition for any $t:T$,
  then we say that $P$ is a \emph{decidable predicate} on $T$.
\end{definition}

Given a type $T$ and a function $f: T\to\bool$,
\cref{lem:isset-bool} yields that $f(t) \eq \yes$ is a
proposition, and we can form the predicate $P(t)\defeq (f(t) \eq \yes)$.
Then $P: T\to\Prop$ is a decidable predicate by \cref{xca:decidability}. 
However, not every predicate can be given through a $f: T\to\bool$, since
$\Prop$ and $\bool$ are only equivalent if LEM holds (\cref{xca:lem-prop}).

In the special case that $P: T\to\UU$ is a decidable predicate
we can define $\chi_P: T\to\bool$ by induction (actually, only case distinction)
on $d(t) :P(t)\amalg\neg P(t)$, setting $\chi_P(t) \eq \yes$
if $d(t)\jdeq\inl{\_}$ and $\chi_P(t) \eq \no$ if $d(t)\jdeq\inr{\_}$.
In this way, decidable predicates on a type $T$ correspond to
their characteristic functions $T\to\bool$.

\begin{xca}\label{xca:decidability}
Show that $f(t) \eq \yes$ is a decidable predicate on $T$,
for any type $T$ and function $f:T\to\bool$.
Show that $(P\equivto\true)\amalg(P\equivto\false)$ holds
for every decidable proposition $P$.
\end{xca}

\begin{definition}\label{def:subtype}
  Let $T$ be a type.
  The type of \emph{subtypes}\index{subtype} of $T$,
  denoted by $\Sub(T)$, is defined by
  \[
  \Sub(T) \defeq (T\to\Prop).
  \]
  \glossary[Subtype]{$\protect\Sub(T)$}{the type of subtypes of $T$}
  \index{subtype}
  Given a predicate $P$ on $T$, we define $T_P\defeq \sum_{t:T} P(t)$
  to be the \emph{underlying type} of the subtype of $T$ characterized by $P$.
  \end{definition}

The following lemma states that identity types in a subtype\footnote{%
The phrase `subtype' is often used for `underlying type of the subtype'.
See \cref{ft:caution-subtype} for when it is important
to be precise.}
are equivalent to those in the type itself.

\begin{lemma}\label{lem:subtype-eq-=}
  Let $T$ be a type and $P: T\to\Prop$ a predicate on $T$.
  Recall the underlying type $T_P \jdeq \sum_{t:T}P(t)$, and
  consider the projection map $\fst$ from $T_P$ to $T$.
  Then $\ap{\fst}: ((x_1,p_1) \eqto (x_2,p_2)) \to (x_1 \eqto x_2)$ is an
  equivalence, for any elements $(x_1,p_1)$ and $(x_2,p_2)$ of $T_P$.
\end{lemma}

\begin{proof}
\cref{cor:contract-away} gives that $\inv\fst(t)\weq P(t)$ for all $t:T$,
so that $\fst$ is an injection. Now apply \cref{lem:inj-ap}. 
\end{proof}

\begin{remark}\label{rem:subtype-convention}
  A very convenient consequence of~\cref{lem:subtype-eq-=}
  is that we can afford not to distinguish carefully
  between elements $(t,p)$ of the subtype $T_P$
  and elements $t$ of type $T$ for which the proposition $P(t)$ holds.
  We will hence often silently coerce from $T_P$ to $T$ via the first projection,
  and if $t:T$ is such that $P(t)$ holds, we'll write $t:T_P$
  to mean any pair $(t,p)$ where $p:P(t)$,
  since when $P(t)$ holds, the type $P(t)$ is contractible.
\end{remark}

\begin{example}\label{def:Prop-Set}
The type of types that are propositions and the
type of types that are sets are defined as:
\[\Prop_\UU\defeq \sum_{X:\UU}\isprop(X)\quad
\text{and}\quad\Set_\UU\defeq \sum_{X:\UU}\isset(X).\]
\glossary[Prop]{$\Prop$}{the type of propositions}
\glossary[Set]{$\Set$}{the type of sets}

Both $\Prop_\UU$ and $\Set_\UU$ are subtypes of $\UU$, and
both are types in a universe one higher than $\UU$.
We just write $\Prop$ and $\Set$ when we don't care about the 
precise universe $\UU$.

Following the convention in \cref{rem:subtype-convention},
when we have a type $A$ for which we know that it is a proposition (or a set),
we simply write $A : \Prop$ (or $A : \Set$).
\end{example}

\begin{lemma}\label{lem:Prop-in-Set}
The proposition $\isset(\Prop)$ holds, that is, $\Prop$ is a set.
\end{lemma}
\begin{proof}
We show that $P\eqto Q$ is a proposition for all propositions $P$ and $Q$.
By univalence, $P\eqto Q$ is equivalent to 
$(P\equivto Q)\jdeq\sum_{f:P\to Q}\isEq(f)$.
The latter is a proposition by \cref{lem:prop-utils}\ref{prop-utils-codom}\ref{prop-utils-sum}, using that $\isEq(f)$ is a proposition.
\end{proof}

Since $\Prop$ is a set, $\Sub(T)$ is also a set, for any type $T$.\footnote{%
\label{ft:caution-subtype}
Caution: When identifying `subtypes', it
should be clear whether they are considered as elements of $\Sub(T)$ or
as underlying types of subtypes, \ie as elements of some universe $\UU$.
The identity types $P\eq_{\Sub(T)} Q$ and $T_P\eqto_{\UU} T_Q$ are in general
not equivalent!}

\begin{xca}\label{xca:subtype-univ-prop}
  Let $T$ and $X$ be types, $f: X\to T$ a function,
  and $P : T\to\Prop$ a predicate. Show that $\prod_{x:X} P(f(x))$
  holds if and only if the following type\footnote{\label{ft:subtype-univ-prop}%
    \[
      \begin{tikzcd}[ampersand replacement=\&]
        X \ar[dd,dashed,"g"']\ar[r,"f"] \& T \\
        \\
        \sum_{t:T} P(t) \ar[uur,"{\fst}"']
      \end{tikzcd}
    \]}
  is contractible:
   \begin{displaymath}
    \sum_{g: X \to \sum_{t:T} P(t)} f \eqto \fst\circ g.\qedhere
  \end{displaymath}
\end{xca}

We call the result in \cref{xca:subtype-univ-prop} the 
\emph{universal property of subtypes}.\footnote{%
In set theory, if $S\subseteq T$ and $f: X\to T$ is such that
$f(x)$ is in $S$ for all $x$ in $X$, then $x\mapsto f(x)$ is the
unique function $g: X\to S$ such that $f=i\circ g$, where $i$ is the
inclusion map of $S$ in $T$.}

A pair like $(T_P,\fst)$ in \cref{lem:subtype-eq-=} is actually an 
example of the second approach to subtypes, which we will explain now.  

\begin{definition}\label{def:injtype}
  A \emph{injection into a type}\index{injection!into a type} $T$
  is a type $S$ together with an injection $f : S \to T$.%
  \glossary(Injinto){$\protect\Inj(T)$}{type of injections into $T$}
  The type $S$ is called the \emph{underlying type} of the injection into $T$.%
  \footnote{Instead of using this tedious phrase, we will simply call $S$
  a `subtype' of $T$, if the injection is clear from the context.
  The cautioning \cref{ft:caution-subtype} applies here as well.}
  Selecting a universe $\UU$ as a repository for such types $S$ allows
  us to introduce the type of injections into $T$ in $\UU$ as follows.
  \[
  \Inj^\UU(T) \defeq \sum_{S:\UU}\sum_{f:S\to T}\isinj(f).
  \]
  \glossary[Inj]{$\protect\Inj(T)$}{equivalent type of subtypes of $T$}
  \index{subtype}
  When no confusion can arise, we simply write $\Inj(T)$ for $\Inj^\UU(T)$.
\end{definition}

\begin{lemma}\label{lem:Sub(T)=Inj(T)}
The function mapping any subtype $P$ of $T$ to the injection 
$\fst: T_P\to T$ defines an
equivalence from $\Sub(T)$ to $\Inj(T)$, for any type $T$.
The inverse equivalence maps any injection $i:S\to T$ to 
the subtype $(t\mapsto \inv i (t))$ of $T$.
\end{lemma}
\begin{proof}
We postpone the proof till \cref{lem:Prop-Set-pointed-families}
\ref{lem:Prop-families}, where this and similar results are obtained 
by a general method. If you just can't wait, do \cref{xca:Sub(T)=Inj(T)}.
\end{proof}

As a consequence, $\Inj(T)$ is a set since $\Sub(T)$ is, for any type $T$.
\stepcounter{footnote}\footnotetext{\label{ft:incl-vs-inj}
The full notation as an element of $\Inj(T)$
would be $(\setof{t:T}{P(t)},\fst,p)$,
with $p$ witnessing that $\fst$ is an injection.
In traditional set theory one would call $\fst$ the inclusion
of the subset, which is unique for each subset.
In contrast, there can be \emph{many} pairs $(X,i)$, with $i: X\to T$
an injection, defining the same subset of $T$. If in set theory
one would define subsets through such pairs, one would have
to solve a size issue and define an equivalence relation
such that equivalent pairs define the same subset.
In type theory, however,
we have universes, and the identity type of $\Inj^\UU(T)$ identifies
precisely the triples defining the same subset.

Such considerations also apply to subtypes, and
later to subgroups in \cref{def:typeofmono}.
}\addtocounter{footnote}{-1}

\begin{xca}\label{xca:Sub(T)=Inj(T)}
Prove \cref{lem:Sub(T)=Inj(T)}. Hints: %use \cref{lem:weq-iso}.
For the round trip starting with $P$, use function extensionality and
\cref{cor:contract-away}. For the round trip starting with $(S,i)$,
show that the function $g$ in \cref{ft:subtype-univ-prop} is an equivalence
in case $X\jdeq S$, $f\jdeq i$ is an injection, and $P\jdeq\inv i(\blank)$.
\end{xca}

\cref{lem:subtype-eq-=} has other important consequences:
\begin{corollary}\label{cor:subtype-same-level}
  For any $n\geq -1$,
  if $T$ is a $n$-type, then $T_P$ is also a $n$-type.
\end{corollary}
In particular, if $T$ is a set, then $T_P$ is again a set;
we then call $T_P$ a \emph{subset} of $T$ and we may denote it by
$\setof{t:T}{P(t)}$.\footnotemark
\glossary(subset){$\setof{t:T}{P(t)}$}{set comprehension}
\index{set!comprehension}

\begin{xca}\label{xca:subsets-inclusion}
  Let $T$ be a set. 
  Define the relation ${\subseteq}: (\Sub(T)\times\Sub(T))\to\Prop$ 
  by $(P_0 \subseteq P_1) \defeq \prod_{t:T}(P_0(t)\to P_1(t)$.\footnote{%
  Recall that we can move without notice between 
  $(\Sub(T)\times\Sub(T))\to\Prop$ and $\Sub(T)\to\Sub(T)\to\Prop$.} 
  Prove that the relation ${\subseteq}$ is a partial
  order\footnote{\label{ft:partial-order}%
    Recall that an \emph{partial order} on a set $S$ is a relation $R$ that is
    (1)~\emph{reflexive}: $R(x,x)$,
    (2)~\emph{transitive}: $R(x,y) \to R(y,z) \to R(x,z)$, and
    (3)~\emph{antisymmetric}: $R(x,y) \to R(y,x) \to x\eq y$.}
  with a least and a greatest element (even if $T$ is the empty type).
\end{xca}

\begin{definition}\label{def:decidable-set}\index{decidable set}
  A type $A$ is called a \emph{decidable set} if the identity type $x \eqto y$
  is a decidable proposition for all $x,y:A$.
\end{definition}
Note the slight subtlety of this definition together with
\cref{def:decidability}: Any proposition has decidable identity types
(since each instance is contractible) and is thus a \emph{decidable set},
even though it may not be \emph{decidable as a proposition}.

The way we phrased this definition implies that $A$ is a set.
The following celebrated and useful theorem states that this is unnecessary.
\begin{theorem}[Hedberg]\label{thm:hedberg}\index{Hedberg's theorem}
  Any type $A$ for which we have a function of type
  $\prod_{x,y:A}\bigl((x \eqto y) \amalg \lnot(x \eqto y)\bigr)$
  is a decidable set.
\end{theorem}
For a proof see~Theorem~7.2.5 of the HoTT Book\footcite{hottbook}.

\section{Pointed types}\label{sec:pointedtypes}
Sometimes we need to equip types with additional structure
that cannot be expressed by a proposition such as
$\isprop(X)$ and $\isset(X)$ above.
Therefore the following is \emph{not} a subtype of $\UU$.

\begin{definition}\label{def:pointedtypes}
  A \emph{pointed type} is a pair $(A,a)$ where $A$ is a type
  and $a$ is an element of $A$. The \emph{type of pointed types} is%
  \index{pointed type}\glossary(UUb){$\protect\UUp$}{universe of pointed types, \cref{def:pointedtypes}}
  \[
    \UUp \defeq \sum_{A:\UU} A.
  \]
  Given a type $A$ we let $A_+$ be the pointed type you get
  by adding a default element:
  $A_+\defequi(A\amalg\true,\inr{\triv})$.%
  \glossary(1plus){$A_+$}{$A$ together with a disjoint base point}
  Given a pointed type $X\jdeq(A,a)$,
  the \emph{underlying type}%
  \glossary(1div){$A_\div$}{underlying type of a pointed type $A$}
  is $X_\div\defeq A$,\footnote{%
    The \emph{obelus}\index{obelus} $\div$ is sometimes used to denote division,
    but is also used to for subtraction, especially in Northern Europe.
    This inspired our use, considering its ``adjoint'' relationship
    to $+$ detailed in~\cref{xca:plusforgetadjoint}.}
  and the \emph{base point}%
  \index{base point}%
  \glossary(pt){$\pt_X$}{base point of a pointed type $X$}
  is $\pt_X\defeq a$,
  so that $X\jdeq (X_\div,\pt_X)$.

  Let $X \defeq (A,a)$ and $Y\defeq(B,b)$ be pointed types.
  Define the map  $\ev_a : (A\to B)\to B$ by $\ev_a(f)\defeq f(a)$.
  Then the fiber of $\ev_a$ at $b$ is the type
  $\ev_a^{-1}\jdeq\sum_{f:A\to B}(b \eqto f(a))$. The latter type is also
  called the type of \emph{pointed functions} from  $X$ to $Y$
  and denoted by $X\ptdto Y$. In the notation above,
  \[
    (X\ptdto Y) \jdeq \sum_{f:X_\div\to Y_\div}(\pt_{Y} \eqto f(\pt_X)).
  \]
  Given a pointed function $g \jdeq (f,p)$, the \emph{underlying function}
  is $g_\div \defeq f$, and the \emph{pointing path}\index{pointing path}
  is $g_\pt \defeq p$, so that $g \jdeq (g_\div,g_\pt)$.

  If $Z$ is also a pointed type,
  and we have pointed functions $f : X\ptdto Y$ and $g : Y\ptdto Z$,
  then their composition
  $gf : X\ptdto Z$ is defined as the pair $(g_\div f_\div,g_\div(f_\pt)g_\pt)$,
  as illustrated below.\footnote{%
    In particular, $(gf)_\div \jdeq g_\div f_\div$.}
  \[
    \begin{tikzcd}[baseline=(O.base)]
      & \pt_Y \ar[r, eqr, "f_\pt"]\ar[d, mapsto, "g_\div"]
      & f_\div(\pt_X) \ar[d, mapsto, "g_\div"]\\
      \pt_Z \ar[r, eqr, "g_\pt"] & g_\div(\pt_Y) \ar[r, eqr, "g_\div(f_\pt)" ] &
      |[alias=O]| g_\div(f_\div(\pt_X))
    \end{tikzcd}
  \]
  We may also use the notation $g \circ f$ for the composition.
\end{definition}

\begin{definition}\label{def:pointedidentity}
  If $X \jdeq (A,a)$ is a pointed type, then we define the \emph{pointed identity map}
  $\id_X : X \ptdto X$ by setting $\id_X \defeq (\id_A, \refl a)$.
\end{definition}

\begin{remark}\label{rem:coerceawaypt}
If $X$ is a pointed type, then $X_\div $ is a type, but $X$ itself is
\emph{not} a type. It is therefore unambiguous, and quite convenient,
to write $x:X$ for $x:X_\div$, and $X\to\UU$ for $X_\div\to\UU$.
Likewise, we can write $f : X \to Y$ for $f_\div : X_\div \to Y_\div$.
In that case we still write $f_\pt : \pt_X \eqto f(\pt_Y)$ for the
witness of pointedness.
\end{remark}

\begin{xca}\label{xca:plusforgetadjoint}
If $A$ is a type and $B$ is a pointed type,
give an equivalence from $A\to B_\div$ to $A_+\ptdto B$.
\end{xca}

\begin{xca}\label{xca:freemaps}
  Let $A$ be a pointed type and $B$ a type. Give an equivalence from
  $\sum_{b:B}(A\ptdto (B,b))$ to $(A_\div\to B)$.
\end{xca}

Since $\UUp$ and $X\ptdto Y$ are sum types, the results on identifying pairs
in \cref{sec:pairpaths} apply to pointed types and pointed maps as well.

\begin{definition}\label{def:pointedequiv}
  If $X$ and $Y$ are pointed types, we define the type of pointed equivalences
  from $X$ to $Y$ as:
  \[
    X \ptdweto Y \defeq \sum_{f : X \ptdto Y}\isEq(f_\div)\qedhere
  \]
\end{definition}
\begin{xca}\label{xca:pointedequiv}
  From an identification of pointed types $p : X \eqto Y$,
  construct an identification of the underlying types, $p_\div : X_\div \eqto Y_\div$,
  as well as an identification $q : \pt_Y \eqto \ptoe p_\div(\pt_X)$.
  Together, this gives a map of type
  \[
    (X \eqto Y) \to (X \ptdweto Y).
  \]
  Show that this is an equivalence.
\end{xca}

\section{Operations that produce sets}
\label{sec:operations-on-sets}

The following lemma holds for $n$-types in general,
but we only need it for propostions and sets.

\begin{lemma}\label{lem:Set-is-groupoid}
Let $X$ and $Y$ be types.
\begin{enumerate}
\item
If $X$ and $Y$ are propositions, then so are $X \equivto Y$ and $X \eqto Y$.
In other words, $\Prop$ is a set.
\item
If $X$ and $Y$ are sets, then so are $X \equivto Y$ and $X \eqto Y$.
In other words, $\Set$ is a groupoid.
\end{enumerate}
\end{lemma}

\begin{proof}
 By univalence, $X \eqto Y$ and $X\equivto Y$ are equivalent,
 whereas the latter is equal by definition to $\sum_{f:X\to Y} \isEq(f)$.
 If $X$ and $Y$ are propositions (sets),
 then by \cref{lem:level-n-utils} also $X\to Y$ is a proposition (set).
 Moreover, $\isEq(f)$ is a proposition by \cref{lem:isX-is-prop}.
 Now the lemma follows by \cref{cor:subtype-same-level}.
\end{proof}

One may wonder whether $\NN$ as defined in \cref{sec:inductive-types}
is a set. The answer is yes, but it is harder to prove than one
would think. In fact we have the following theorem.

\begin{theorem}\label{thm:isset-inductive-types}
All inductive types in \cref{sec:inductive-types} are sets
if all constituent types are sets.
\end{theorem}

\begin{proof}
  We only do the case of $\NN$ and leave the other cases to the reader
  (cf.\ \cref{xca:set-sum}). The following proof is due to Simon Huber.
  We have to give identifications of type $p \eqto q$ for all $n,m : \NN$
  and $p, q : n \eq m$.
  By induction on $q$ it suffices to give identifications of type
  $p \eqto \refl n$ for all $p : n \eqto n$.
  Note that this cannot simply be done by induction on $p$.
  Instead we first give an inversion principle for
  identifications in $\NN$ as follows. Define a type $T(n,m,p)$
  for $n, m : \NN$ and $p : n \eq m$ by induction on $n$ and $m$:
  \[
    T(0,0,p) \defeq (p \eqto \refl{0})%
    \text{~and~}%
    T(\Succ(n), \Succ(m), p) \defeq \inv{\ap{\Succ}}(p),%
  \]
  and for the other cases the choice does not matter,
  say $T(0, \Succ(m), p) \defeq T(\Succ(n), 0 ,p) \defeq \emptytype$.
  Next we give elements of type $T(n,m,p)$
  for all $n,m$, and $p$ by induction on $p$, reducing to
  $T(n,n,\refl{n})$ for all $n : \NN$, which we deal with by
  distinguishing cases on $n$.
  For $n\jdeq 0$ we use $\refl{\refl{0}}$ and for the case $\Succ(n)$
  we use the pair $(\refl{n},\refl{\refl{\Succ(n)}})$,
  noting that $\ap{\Succ}(\refl{n}) \jdeq \refl{\Succ(n)}$.

  We can now give identifications of type $p \eqto \refl{n}$ for all
  $p : n \eqto n$ by induction on $n$.
  For $n\jdeq 0$ we use the element of  $T(0,0,p)$ constructed above.
  For the case $\Succ(n)$, the element of $T(\Succ(n),\Succ(n),p)$
  constructed above yields a pair $(q,r)$ with $q : n \eqto n$ and
  $r: p \eqto \ap{\Succ}(q)$. By induction hypothesis we have
  and identification $e : q \eqto \refl{n}$. We get the desired
  identification by concatenating $r$ and $\ap{\ap{\Succ}}(e)$:
  \[
    p \eqto \ap{\Succ}(q) \eqto \ap{\Succ}(\refl{n}) \jdeq \refl{\Succ(n)}.
    \qedhere
  \]
\end{proof}

\begin{xca}\label{xca:set-sum}
Show that $X\amalg Y$ is a set if $X$ and $Y$ are sets.
\end{xca}

Recall that propositional truncation is turning any type into
a proposition by adding identifications of any two elements.
Likewise, there is a operation turning any type into a set
by adding (higher) identifications of any two identifications
of any two elements. The latter operation is called set truncation.
It is yet another example of a higher-inductive type.

\begin{definition}\label{def:set-truncation}
Let $T$ be a type. The \emph{set truncation} of $T$
is a type  $\Trunc{T}_0$ defined by the following constructors:
\begin{enumerate}
\item an \emph{element} $\trunc{t}_0 : \Trunc{T}_0$ for all $t:T$;
\item a \emph{identification} $p \eqto q$ for all $x,y:\Trunc{T}_0$ and $p,q: x \eqto y$.
\end{enumerate}
The (unnamed) second constructor ensures that $\Trunc{T}_0$ is a
set. The induction principle states that,
for any family of sets $S(x)$ defined for each $x:\Trunc{T}_0$,
in order to define a function $f:\prod_{x:\Trunc{T}_0} S(x)$,
it suffices to give a function $g: \prod_{t:T} S(\trunc{t}_0)$.
Computationally, we get $f(\trunc{t}_0)\jdeq g(t)$ for all $t:T$.
\end{definition}

In the non-dependent case we get that for any set $S$ and
any function $g: T\to S$ there is a (unique) function $f:\Trunc{T}_0\to S$
satisfying $f(\trunc{t}_0)\jdeq g(t)$ for all $t:T$.\footnote{%
Lemma~7.3.12\footnotemark gives an equivalence from
$\trunc{t}_0 \eq \trunc{t'}_0$ to $\Trunc{t \eqto t'}$ for all $t,t:T$.}%
\footcitetext{hottbook}
A consequence of this recursion principle is that,
for any set $S$, precomposition with $\trunc{\_}_0$ is an equivalence
\[
(\Trunc{T}_0 \to S) \quad \to \quad (T \to S).
\]
This is called \emph{the universal property of set truncation}.\footnote{%
More generally, there are operations turning any type into an $n$-type,
satisfying a similar universal property as propositional truncation
and set truncation. We denote these operations
by $\Trunc{\blank}_n$ with corresponding constructor $\trunc{\blank}_n$.
Propositional truncation $\Trunc{\blank}$ can thus also be denoted as
$\Trunc{\blank}_{-1}$. Sometimes it is convenient to consider
contractible types as $-2$-types, with constant truncation operator
$\Trunc{T}_{-2}\defeq\true$ and
constructor $\trunc{t}_{-2}\defeq\triv$.
}%endmarginnote

\begin{xca}\label{xca:sum-of-conn-components}
  Let $A$ be a type. Define for every element $z : \Trunc{A}_0$
  the connected component corresponding to $z$, $A_{(z)}$,
  a subtype of $A$, such that for $a:A$, you recover the notion from
  \cref{def:connected}: $A_{(\trunc{a}_0)} \jdeq A_{(a)}$.\footnote{%
    \emph{Hint:} Use maps $\Trunc{a \eqto {\blank}} : A \to \Prop$
    and the fact that the universe of propositions
    is a set.}

  Prove that the set truncation map $\trunc{\blank}_0 : A \to \Trunc{A}_0$
  in this way exhibits $A$ as the sum of its connected components,
  parametrized by $\Trunc{A}_0$:
  \[
    A \equivto \sum_{z : \Trunc{A}_0} A_{(z)}.
  \]
  Prove that $A$ is connected iff $\Trunc{A}_0$ is contractible.
\end{xca}

\subsection{Weakly constant maps}

The universal property of the propositional truncation,~\cref{def:prop-trunc},
only applies directly to construct elements of \emph{propositions} (that is, to prove them).
Here we discuss how we can construct elements of \emph{sets}.

\begin{definition}
  A map $f: A \to B$ is \emph{weakly constant} if $f(x) \eqto f(x')$ for all $x,x':A$.
\end{definition}
This is in contrast to a \emph{constant} map,
which can be identified with one of the form $x \mapsto b$ for some $b:B$.
Any constant map is indeed weakly constant.
Note also that when $B$ is a set,
weak constancy of $f : A \to B$ is a proposition.

\begin{theorem}\label{thm:wconstant-elim}
  If $f : A \to B$ is a weakly constant map, and $B$ is a set, then
  there is an induced map $g : \Trunc{A} \to B$ such that
  $g(\trunc x)\jdeq f(x)$ for all $x:A$.
\end{theorem}
\begin{proof}
  Consider the image factorization (\cref{xca:unique-fact-image})
  $A \xrightarrow{p}{} \im(f) \xrightarrow{i}{} B$ of $f$,
  where $p(x) \defeq (f(x),\trunc{(x,\refl{f(x)})})$
  and $i(y,\blank) \defeq y$.

  The key point is that $\im(f)$ is a proposition because
  $f$ is weakly constant. First note that $\im(f)$ is a set
  by \cref{xca:prop-image-is-set}.
  Let $(y_1,z_1),(y_2,z_2):\im(f)$. We have to prove
  $(y_1,z_1) \eq (y_2,z_2)$, which is a proposition.
  Hence we may hypothesize (by truncation induction on $z_i$)
  that we have $x_1,x_2:A$ with $y_i \eq f(x_i)$ for $i=1,2$.
  Hence we get $y_1 \eq f(x_1) \eq f(x_2) \eq y_2$ and
  therefore $(y_1,z_1) \eq (y_2,z_2)$.

  Thus, by the universal property of the truncation,
  we get $g' : \Trunc A \to \im(f)$ such
  that $g'(\trunc x) \jdeq p(x) \jdeq (f(x),\trunc{(x,\refl{f(x)})})$.
  Composing with $i$ we get $g\defeq i\circ g' : \Trunc A \to B$
  with $g(\trunc x) \defeq f(x)$, as desired.
\end{proof}

\subsection{Set quotients}

As an example, we first present an abstraction of the possible
economical situations of a person as a quotient.
Net worth can be defined as wealth minus debt.\marginnote{%
  \begin{tikzpicture}
  \filldraw[fill=casblue!30] (0,0) rectangle (.5,1.5);
  \draw [decorate, decoration = {brace,raise=5pt}] (.5,1.5) --  (.5,0);
  \coordinate [label=right:{wealth $w$}] (w) at (.8,.75);
  \filldraw[fill=casred!30] (0,0) rectangle (.5,-2);
  \draw [decorate, decoration = {brace,raise=5pt}] (.5,0) --  (.5,-2);
  \coordinate [label=right:{debt $d$}] (d) at (.8,-1);
  \draw[thick] (-.25,0) -- (2.5,0);
\end{tikzpicture}}
Let's assume wealth $w$ and debt $d$ are natural numbers.
The debt can be greater than the wealth, yielding a negative net worth,
but at this point in our book we do not have negative numbers at our disposal.
However, we do have the binary product, and the pair
$(w,d): (\NN\times\NN)$ also completely determines the net worth.
However, $(w,d)$ contains more information than necessary for the net worth:
$(\Succ(w),\Succ(d))$, for example, determines the same net worth
as $(w,d)$, and $(\Succ(w),\Succ(d))\ne(w,d)$. Put differently,
the type $\NN\times\NN$ does not capture the notion of net worth,
since its identity types don't capture equality of net worth.

Clearly, we need a different type to capture the notion of net worth.
Of course, we want a type construction that works not only for
the special case of net worth, but also in similar situations.
Common to such situations is that we have a type $A$ and an
equivalence relation\footnote{\label{ft:equiv-rel}%
  Recall that an \emph{equivalence relation} is one that is
  (1) \emph{reflexive}: $R(x,x)$,
  (2) \emph{symmetric}: $R(x,y) \to R(y,x)$, and
  (3) \emph{transitive}: $R(x,y) \to R(y,z) \to R(x,z)$.}
$R : A\to A\to \Prop$. In the example of net worth, we have
$A\defeq(\NN\times\NN)$, and the equivalence relation is
$R((w_1,d_1),(w_2,d_2)) \defeq  (w_1+d_2 = w_2 + d_1)$,
precisely capturing equality of net worth, $w_1 - d_1 = w_2 - d_2$,
without actually using subtraction and negative numbers.

What we need is a new type, which is like $A$, but with $R$ as equality.
Note that the latter requires that the new type is a set.
The quotient set $A/R$ that we will define and study in this
section fulfills these requirements.
In the special case of $A\defeq(\NN\times\NN)$, and
$R((w_1,d_1),(w_2,d_2)) \defeq  (w_1+d_2 = w_2 + d_1)$,
the type $A/R$ could in fact be used as a type of integers,
cf.\ \cref{sec:integers} and see \cref{xca:ints-as-quotient}.

\begin{definition}\label{def:quotient-set}
Given a type $A$ and an equivalence relation
$R : A \to A \to \Prop$,
we define the \emph{quotient set}\footnote{%
  We may wonder about the universe level of $A/R$,
  assuming $A : \UU$ and $R : A \to A \to \Prop_\UU$.
  By the Replacement~\cref{pri:replacement},
  $A/R$ is essentially $\UU$-small, since $A\to\Prop_\UU$
  is locally $\UU$-small. Alternatively, we could use
  Propositional Resizing~\cref{pri:prop-resizing} to push
  the values of $R$ into a lower universe.}
$A/R$ as the image of the map $R : A \to (A \to \Prop)$.
Indeed, $A/R$ is a set, since $\Prop$ is a set, and so are $A\to\Prop$
and the image $\sum_{P:A\to\Prop}\exists_{a:A}(P\eq R(a))$ of $R$.
For $a:A$ we define $[a] \defeq (R(a),\trunc{(a,\refl{R(a)})})$ in $A/R$;
$[a]$ is called the \emph{equivalence predicate of} $a$.\footnote{%
In set theory, $A$ would be a set and the equivalence relation $R$
would be a subset of $A\times A$, satisfying the conditions
in \cref{ft:equiv-rel}.
Equivalence \emph{classes} would be subsets of $A$.

Our definition may look different, but is actually
a natural generalization of the definition in set theory
to type theory. First, we let $A$ be an arbitrary type.
Note that $R\mapsto(z\mapsto R(\fst(z))(\snd(z))$ is an 
equivalence from $A\to(A\to\Prop)$ to $(A\times A)\to\Prop)$.
So, indeed
the equivalence relation $R$ corresponds to a subtype of $A\times A$.

Note further that $\fst([a])\jdeq R(a)$ and that $\snd([a])$ certifies
the (obvious) fact that $R(a)$ is in the image of $R$.
For each $a:A$, the predicate $R(a): A\to\Prop$ is a subtype of $A$.
Therefore we call $[{\color{casred}{a}}]$ the \emph{equivalence
predicate} (instead of \emph{class}) of ${\color{casred}{a}}$,
which is true \emph{for} ${\color{casblue}{a}}$
since $R({\color{casred}{a}})({\color{casblue}{a}})$,
that is, by reflexivity.

We will use $[a]$ and $R(a)$ interchangeably.}
\end{definition}
Any element of the image of $R$ is merely an equivalence predicate:
a predicate $P$ on $A$ for which there exists $a:A$
such that $P(x)$ holds if and only if $R(a,x)$ holds.

In the following proofs we frequently use \cref{xca:all-prop-image}.

\begin{lemma}\label{lem:equiv-class-prop}
  For any equivalence predicate $P : A/R$ and $a:A$,
  $P$ and $[a]$ are equal if and only if $P(a)$ holds.
\end{lemma}
\begin{proof}
  Assume $P$ and $[a]$ are equal.
  Then $P(x)$ iff $R(a,x)$ for all $x:A$. Now
  take $x\defeq a$ and use reflexivity $R(a,a)$ to conclude $P(a)$.

  Conversely, assume $P(a)$, and let $x:A$ be given.
  To prove the proposition $P(x) \eq R(a,x)$ we may assume that
  $P \jdeq [b]$ for some $b:A$.
  Then $P(x) \jdeq R(b,x)$, and we need to show $R(b,x) \eq R(a,x)$.
  This follows from $P(a) \jdeq R(b,a)$ using symmetry and transitivity.
\end{proof}

The following theorem gives two important properties of the set quotient,
the second is commonly called the universal property.

\begin{theorem}\label{thm:quotient-property}
  We have $[x] \eq [x']$ if and only if $R(x,x')$ for all $x,x':A$.
  Also, let $B$ be a \emph{set} and $f : A \to B$ a
  function such that $f(x) \eq f(x')$ for all $x,x':A$ such that $R(x,x')$.
  Then the type $\sum_{g: A/R \to B} (f \eq g\circ[\blank])$ is
  contractible.\footnote{In a diagram:
  \[\begin{tikzcd}[column sep=small,ampersand replacement=\&]
    A \ar[r,"f"] \ar[d,"{[\blank]}"'] \& B \\
    A/R \ar[ur,"g"']
  \end{tikzcd}\]}
\end{theorem}
We will construct the center of contraction $\bar f : A/R \to B$
such that $\bar f([x]) \jdeq f(x)$ for all $x:A$.
\begin{proof}
  For the first part we use \cref{lem:equiv-class-prop}
  applied to $P_x \defeq [x]$ and $x'$.

  Now let $B$ be a set and let $f : A \to B$ a function
  satisfying $f(x) \eq f(x')$ for all $x,x':A$ such that $R(x,x')$.
  We first define the center of contraction $\bar f : A/R \to B$.
  Let $z\jdeq(P,p):A/R$. To define $\bar f(z)$ in $B$,
  we note that $f \circ \fst$ is a weakly constant map
  of type $\sum_{x:A}(P \eq [x]) \to B$. By \cref{thm:wconstant-elim}
  we get a map $g: \exists_{x:A}(P \eq [x]) \to B$ and we put
  $\bar f(z)\defeq g(p)$.

  We check the equality by definition: As an element of $A/R$,
  equivalence predicate $[x]$ is accompanied by the witness
  $p\jdeq \trunc{(x, \refl{[x]})} : \exists_{y:A}([x] \eq [y])$.
  By~\cref{thm:wconstant-elim}, this is mapped by $g$, by definition,
  to $(f \circ \fst)(x, \refl{[x]}) \jdeq f(x)$, as desired.

  Now, if $g,h$ satisfy $g\circ[\blank] \eq f \eq h\circ[\blank]$,
  then for any $z:A/R$, the type $g(z) \eq h(z)$ is a proposition
  since $B$ is a set, so we may assume $z\jdeq [x]$ for some $x:A$.
  Then $g([x]) \eq f(x) \eq h([x])$, as desired.
\end{proof}

\begin{xca}\label{xca:A/True-prop-trunc}
Give an equivalence $A/R \to \Trunc{A}$ when $R(x,y)\defeq\true$
for all $x,y:A$.\footnote{%
  If $A$ is a finite set, we can picture this relation as a complete
  symmetric graph, \ie with an edge between every pair of nodes, like this:\\
  \begin{center}
    \begin{tikzpicture}
    \foreach \n/\deg in {0/0, 1/72, 2/144, 3/216, 4/288} {
      \node[dot] (x\n) at (\deg:1) {};
    }
    \foreach \n in {1, ..., 4}
      \foreach \m in {0, ..., \n} {
        \draw (x\m) -- (x\n);
    }
    \end{tikzpicture}
  \end{center}
  Convince yourself that a general equivalence relation
  on a finite set looks like a union of such complete graphs.}
\end{xca}

\begin{xca}\label{xca:ints-as-quotient}
Let $A\defeq(\NN\times\NN)$ and $R: A\to A\to\Prop$ defined by
$R((w_1,d_1),(w_2,d_2)) \defeq  (w_1+d_2 = w_2 + d_1)$.
Let $Z \defeq \set{(w,d)\mid (d=0) \lor (w=0 \land d\ne 0)}$.
Construct an equivalence $f: A/R\to Z$ such that for all
$(w,d,p):Z$ we have $f([(w,d)]) = (w,d)$.
\end{xca}

It is also possible to postulate\footnote{%
\emph{The method of 'postulating' what we want has many advantages;
  they are the same as the advantages of theft over honest toil.}\hfill
\citeauthor{russell-intro-mp}\footnotemark{}}\footcitetext{russell-intro-mp}
the quotient set as a higher inductive type.

\begin{definition}\label{def:quotient-as-HIT}
  Let $A$ be a type and $R : A \to A \to \Prop$ an equivalence relation.
  Define the quotient $A/R$ to be type with the following constructors:
  \begin{enumerate}
  \item a constructor $s$ of type $\isset(A/R)$ ensuring that $A/R$ is a set;
  \item an element constructor $[x] : A/R$ for all $x:A$;
  \item a constructor providing a proof $r(x,y,p)$ of
  $[x] \eq [y]$ for all $x,y : A$ and $p:R(x,y)$.
  \end{enumerate}
  Let $B(z)$ be a set for every element $z:A/R$. The induction principle
  for $A/R$ states that, in order to define an element of $B(z)$
  for every $z:A/R$,
  it suffices to give elements $b_x : B([x])$ for every $x:A$
  together with a proof of the proposition
  $\pathover{b_x}{B}{r(x,y,p)}{b_y}$ for all $x,y:A$ and $p:R(x,y)$.
  The function $f$ thus defined satisfies $f([x])\jdeq b_x$ for all $x:A$.
\end{definition}

\begin{xca}\label{xca:quotients-equivalence}
Give an equivalence between $A/R$ as defined in \cref{def:quotient-set}
and $A/R$ as defined in \cref{def:quotient-as-HIT}.
\end{xca}

\begin{remark}\label{rem:set-trunc-as-quotient}
We can use set quotients to give an alternative definition
of the set truncation $\Trunc{A}_0$ of a type $A$.
Consider the relation $R : A \to A \to \Prop$ given by
$R(x,y) \defeq \Trunc {x \eqto y}$.
This is easily seen to be an equivalence relation,
using $\refl{},\symm$ and $\trans$ from \cref{sec:identity-types}.
Hence we get a quotient set $A/R$ that satisfies
$(\trunc{x}_0 \eq \trunc{y}_0) \equiv \Trunc{x\eqto y}$,
for all elements $x$ and $y$ of $A$,
where we write $\trunc{\blank}_0$ for the equivalence predicates.
Furthermore,~\cref{thm:quotient-property} implies that
$A/R$ satisfies the recursion principle of~\cref{def:set-truncation}:
If $S$ is a set, and $g:A\to S$ is any function,
then $g(x) \eq g(y)$ holds whenever $\Trunc{x\eqto y}$
by the elimination principle
of the propositional truncation,
and hence we get a function $f : A/R \to S$ satisfying
$f(\trunc{x}_0)\jdeq g(x)$ for all $x:A$, as desired.\footnote{%
  Expanding the definitions,
  this means that we can take the $0$-truncation $\Trunc{A}_0$
  of $A:\UU$ to be the $\UU$-small image
  of the $(-1)$-truncated identity relation
  $A \to (A \to \Prop_\UU)$.
  Similarly, we can recursively construct the $(n+1)$-truncation
  by taking the $\UU$-small image
  of the $n$-truncated identity relation
  $A \to (A \to \sum_{X:\UU}\mathrm{is}{n}\mathrm{Type})$.}
\end{remark}

\begin{xca}\label{xca:map-induces-quotient}
Let $A$ and $B$ be types and $f:A\to B$ a function.
Consider the \emph{equivalence relation on $A$ induced by} $f$ 
\index{equivalence relation!induced by map}
given by 
\[
(a\mapsto(a'\mapsto\Trunc{f(a)\eqto f(a')})) : A\to (A\to\Prop).
\]
The corresponding \emph{quotient of $A$ induced by} $f$ is denoted by $A/f$.
\index{quotient!induced by map}
\glossary[A/f]{$A/f$}{quotient induced by $f:A\to B$}
Now:
\begin{enumerate}
\item\label{it:inj-ind-settrunc=domain}
If $f$ is injective, give an equivalence from $A/f$ to $\setTrunc{A}$;
\item\label{it:surj-ind-quot=codomain}
If $B$ is a set and $f$ surjective, give an equivalence from $A/f$ to $B$.\qedhere
\end{enumerate}
\end{xca}

\section{More on natural numbers}
\label{sec:more-on-N}

A useful function $\NN\to\NN$ is the \emph{predecessor} $\Pred$ defined by
$\Pred(0)\defeq 0$ and $\Pred(\Succ(n))\defeq n$.
Elementary properties of addition, multiplication and predecessor
can be proved in type theory in the usual way.
We freely use them, sometimes even in definitions, leaving most of the
proofs/constructions to the reader.

\begin{definition}
\label{def:orderonN}
Let $n,m:\NN$. We say that $m$ is less than or equal to $n$, and write $m\leq n$,
if there is a $k:\NN$ such that $k+m \eq n$. Such a $k$ is unique, and if it
is not $0$, we say that $m$ is less than $n$, denoted by $m<n$.
Both $m\leq n$ and $m<n$ are propositions for all $n,m:\NN$.
\end{definition}

\begin{xca}\label{xca:try-your-luck-N}
Try your luck in type theory proving any of the following.
The successor function satisfies $(\Succ(n) \eq \Succ(m))\liff(n \eq m)$.
The functions $+$ and $\cdot$ are commutative and associative,
$\cdot$ distributes over $+$.
The relations $\leq$ and $<$ are transitive and
preserved under $+$; $\leq$ also under $\cdot$.
We have $(m\leq n) \liff ((m<n)\amalg(m \eq n))$ (so $\leq$ is reflexive).
Furthermore, $((m\leq n)\times (n\leq m)) \liff (m \eq n)$,
and $\neg ((m<n)\times(n<m))$ (so $<$ is irreflexive).
\end{xca}

We can prove the following lemma by double induction.

\begin{lemma}\label{lem:dec-eq+order-N}
The relations $\eq$, $\leq$ and $<$ on $\NN$ are decidable.
\end{lemma}
By Hedberg's \cref{thm:hedberg}, we get an alternate proof that $\NN$ is a set.

We will now prove an important property of $\NN$, called the
\emph{least number principle for decidable, non-empty subsets of} $\NN$.
We give some more details of the proof, since they illustrate an aspect
of type theory that has not been very prominent up to now, namely
the close connection between proving and computing.

\begin{construction}
\label{def:Nwellordered}
Let $P(n)$ be a proposition for all natural numbers $n$.
Define the type $P_{\min}(n)$ expressing that $n$ is the smallest
natural number such that $P(n)$:
\[
P_{\min}(n) \defeq P(n) \times \prod_{m:\NN} (P(m) \to n\leq m)
\]
Then we seek a function
\begin{equation}\label{eqn:min}
\min(P) : \prod_{n:\NN}(P(n)\amalg\neg P(n)) \to
          \exists_{n:\NN} P(n) \to \sum_{n:\NN} P_{\min}(n),
\end{equation}
computing a minimal witness for $P$
from evidence that $P$ is decidable and that a witness exists.
\end{construction}
\begin{implementation}{def:Nwellordered}
First note that $P_{\min}(n)$ is a proposition,
and that all $n$ such that $P_{\min}(n)$
are equal. Therefore the type $\sum_{n:\NN} P_{\min}(n)$
is also a proposition.

Given a function $d(n): P(n)\amalg\neg P(n)$ deciding $P(n)$ for each $n:\NN$,
we define a function $\mu_P:\NN\to\NN$ which,
given input $n$, searches for a $k<n$ such that $P(k)$.
If such a $k$ exists, $\mu_P$ returns the least such $k$,
otherwise $\mu_P(n) = n$.
This is a standard procedure that we will call \emph{bounded search}.
The function $\mu_P$ is defined by induction, setting
$\mu_P(0)\defeq 0$ and
$\mu_P(\Succ(n))\defeq \mu_P(n)$ if $\mu_P(n) < n$.
Otherwise, we set $\mu_P(\Succ(n))\defeq n$ if $P(n)$,
and $\mu_P(\Succ(n))\defeq \Succ(n)$ otherwise, using $d(n)$ to decide,
that is, by induction on $d(n):P(n)\amalg\neg P(n)$.
By design, $\mu_P$ `remembers' where it has found the least $k$ (if so).
We are now done with the computational part and the rest
is a correctness proof.

By induction on $n:\NN$ and $d(n): P(n)\amalg\neg P(n)$ we show
\[
%((\mu_P(n)\leq n) \times (\mu_P(n)<n \to P(\mu_P(n)))).
\mu_P(n)\leq n \quad\text{and}\quad \mu_P(n)<n \to P(\mu_P(n)).
\]
The base case where $n \defeq 0$ is easy. For the induction step,
review the computation of $\mu_P(\Succ(n))$. If $\mu_P(\Succ(n)) = \mu_P(n)$
since $\mu_P(n) < n$, then we are done by the induction hypothesis.
Otherwise, either $\mu_P(\Succ(n)) = n$ and $P(n)$, or $\mu_P(\Succ(n)) = \Succ(n)$.
In both cases we are done.

Also by induction on $n:\NN$ and $d(n): P(n)\amalg\neg P(n)$ we show
\[
P(m) \to \mu_P(n)\leq m,~ \text{for all $m$ in $\NN$.}
\]
The base case $n \defeq 0$ holds since $\mu_P(0) = 0$. For the induction step,
assume $P(m) \to \mu_P(n)\leq m$ for all $m$ (IH). Let $m:\NN$
and assume $P(m)$. We have to prove $\mu_P(\Succ(n))\leq m$.
If $\mu_P(\Succ(n)) = \mu_P(n)$ we are done by IH. Otherwise we have
$\mu_P(n) = n$ and $\mu_P(\Succ(n)) = \Succ(n)$ and $\neg P(n)$.
Then $\mu_P(n)\leq m$ by IH, and $n\ne m$, so $\mu_P(\Succ(n))\leq m$.

By contraposition we get from the previous result
\[
\mu_P(n) = n \to \neg P(m),~\text{for all $m<n$.}
\]

Note that there may not be any $n$ such that $P(n)$;
the best we can do is to prove
\[
P(n)\to P_{\min}(\mu_P(\Succ(n)))
\]
by combining previous results. Assume $P(n)$.
Then $\mu_P(\Succ(n))\leq n < \Succ(n)$, so that $P(\mu_P(\Succ(n)))$.
Moreover, $P(m) \to \mu_P(\Succ(n))\leq m$ for all $m$ in $\NN$.
Hence $P_{\min}(\mu_P(\Succ(n)))$.

Since $\sum_{n:\NN} P_{\min}(n)$ is a proposition,
we obtain the required function by the induction
principle for propositional truncation, \cref{def:prop-trunc}:
\[
\min(P) : \prod_{n:\NN}(P(n)\amalg\neg P(n)) \to
           \Trunc[\Big]{\sum_{n:\NN} P(n)} \to  \sum_{n:\NN} P_{\min}(n).\qedhere
\]
\end{implementation}

\begin{remark}\label{rem:computations-can-decide}
In the interest of readability, we do not always make the use
of witnesses of decidability in computations explicit.
A typical example is the case distinction on $\mu_P(n) < n$ in
\cref{def:Nwellordered} above. This remark applies to all
sets and decidable relations on them. We shall immediately put
this convention to good use in the proof of a form of the so-called
\emph{Pigeonhole Principle} (PHP).
\end{remark}

\begin{lemma}\label{lem:PHP}
For all $N:\NN$ and $f:\NN\to\NN$ such that $f(n)<N$
for all $n<N+1$, there exist $m < n < N+1$ such that $f(n) = f(m)$.
\end{lemma}
\begin{proof}
By induction on $N$. In the base case $N = 0$ there is nothing to do.
For the induction case $N+1$, assume the lemma proved for $N$
(induction hypothesis, IH, for all $f$). Let $f$ be such
that $f(n)<N+1$ for all $n<N+2$. The idea of the proof is
to search for an $n<N+1$ such that $P(n)\defeq (f(n) = N)$,
by computing $\mu_P(N+1)$ as in \cref{def:Nwellordered}.
If $\mu_P(N+1) = N+1$, that is, $f(n)<N$ for all $n<N+1$,
then we are done by IH. Assume $\mu_P(N+1) < N+1$,
so $f(\mu_P(N+1)) = N$.
If also $f(N+1) = N$ then we are done.
If $f(N+1)<N$, then we define $g$ by $g(n) = f(N+1)$
if $f(n) = N$, and $g(n) = f(n)$ otherwise.
Then IH applies to $g$, and we get $m < n < N+1$ with
$g(n) = g(m)$. If $f(n) = f(m)$ we are of course done.
Otherwise, $f(n),f(m)$ cannot both be smaller than $N$,
as $g(n) = g(m)$. In both remaining cases,
$f(n) = g(n) = g(m) = f(N+1)$ and $f(N+1) = g(n) = g(m) = f(m)$,
we are done.
\end{proof}

We can now rule out the existence of equivalences between finite
sets of different size.
\begin{corollary}\label{cor:Fin-n-injective}
If $m<n$, then $(\sum_{k:\NN} k<m) \ne (\sum_{k:\NN} k<n)$.
\end{corollary}

Another application of \cref{def:Nwellordered} is a
short proof of Euclidean division.
\begin{lemma}\label{lem:euclid-div}
  For all $n,m:\NN$ with $m>0$ there exist unique $q,r:\NN$
  such that $r<m$ and $n = qm+r$.
\end{lemma}
\begin{proof}
Define $P(k)\defeq (n\leq km)$. Since $m>0$ we have $P(n)$.
Now set $k\defeq\mu_P(n)$ as in \cref{def:Nwellordered}.
If $n = km$ and we set $q\defeq k$ and $r\defeq 0$.
If $n<km$, then $k>0$ and we set $q\defeq k-1$.
By minimality we have $qm<n<km$ and hence $n = qm+r$ for some $r<m$.
\end{proof}

\section{The type of finite sets}
\label{sec:typeFin}
Recall from \cref{sec:finite-types} the types
$\false$, $\true$ and $\bool$ containing zero, one and two
elements, respectively. We now define generally the
type of $n$ elements for any $n:\NN$.
%$\emptytype$, $\bn{1} $, $\bn{2} ,\ldots$

\begin{definition}\label{def:finiteset}
For any type $X$ define $\Succ(X)\defeq X\amalg\true$.
Define inductively the type family $\Fin(n)$, for each $n:\NN$, by
setting $\Fin(0)\defeq\emptytype$ and $\Fin(\Succ(n))\defeq\Succ(\Fin(n))$.
% Now abbreviate $\bn{n}\defeq\Fin(n)$.
The type $\Fin(n)$ is called
the type with $n$ elements, and we denote its elements
by $0,1,\ldots,n-1$ rather than by the corresponding expressions
using $\inl{}$ and $\inr{}$.

We also define as abbreviation $\bn n \defeq \Fin(n)$ for a natural number $n$,
so $\bn 0 \defeq \Fin(0)$, $\bn 1 \defeq \Fin(1)$, $\bn 2 \defeq \Fin(2)$, etc.
\end{definition}

\begin{xca}\label{xca:finite-types}
\leavevmode
  \begin{enumerate}
  \item Denote in full the elements of $\bn{0}$, $\bn{1} $, and $\bn{2}$.
  \item Construct an equivalence in $\bn{1} \equivto \true$
                         and one in $\bn{2} \equivto \bool$.
  \item Construct equivalences in  $\bn{n} \equivto \sum_{k:\NN} k<n$
        for all $n:\NN$.
  \item Show that $m=n$ if we are given an element of type
        $\bn{m} \eqto \bn{n}$.\qedhere
  \end{enumerate}
\end{xca}
\begin{definition}\label{def:is-finite}
  Given a type $X$, we define the proposition
  \[
    \textstyle
    \isfinset(X) \defeq \exists_{n:\NN}(X \eqto \bn{n})
  \]
  to express that $X$ \emph{is a finite set}.\footnote{%
    When moving beyond sets, there are two different ways
    in which a type can be finite: an \emph{additive}
    way and a \emph{multiplicative} way, but
    it would take us too far afield to define these notions
    here.} % And then to prove that their intersection is finite sets
\end{definition}
\begin{lemma}\label{lem:maxonefinitetype}
For all types $X$ we have:
  \begin{enumerate}
  \item $\sum_{n:\NN} \Trunc{X\eqto\bn{n}}$ is a proposition;%
  \footnote{In other words, an $n:\NN$ such that $\Trunc{X\eqto\bn{n}}$
  is unique if it exists.}
  \item $\sum_{n:\NN} \Trunc{X\eqto\bn{n}}$ if and only if $\isfinset(X)$.
  \end{enumerate}
\end{lemma}
\begin{proof}
\leavevmode
\begin{enumerate}
\item Assume $(n,p),(m,q): \sum_{n:\NN}\Trunc{X\eqto\bn{n}}$.
Then $q\circ\inv{p}: {\bn{n}\eqto\bn{m}}$, so ${n=m}$
by \cref{xca:finite-types}. By \cref{lem:isEq-pair=},
\cref{def:pathover-trp} and the fact that the type of $q$
is a proposition, it follows that $(n,p) \eq (m,q)$.
\item Functions in both directions are easily defined by
using the recursion principle of propositional truncation,
see after \cref{def:prop-trunc}.\qedhere
\end{enumerate}
\end{proof}

%The lemma above remains true if $X$ ranges over $\Set$. MB commented out

\begin{definition}\label{def:groupoidFin}
The \emph{groupoid of finite sets} is defined by\footnote{%
  Here it doesn't matter whether we take the 
  sum over $\Set$ or over $\UU$, since any finite set is a set.
  Hence we also have $\FinSet_n
  \jdeq \Set_{(\bn{n})} \eqto \FinSet_{(\bn{n})}
 \eqto \UU_{(\bn{n})}$.}
\[
  \FinSet\defeq\sum_{S:\Set}\isfinset(S).
\]
\glossary(FinSet){$\protect\FinSet$}{the groupoid of finite sets}
For $n:\NN$, the \emph{groupoid of sets of cardinality $n$} is defined by
\[
  \FinSet_n\defequi \sum_{S:\Set}\Trunc{\bn{n}\eqto S}.
\]
\glossary(FinSetn){$\protect\FinSet_n$}{the groupoid of sets of cardinality $n$}
\cref{lem:maxonefinitetype} yields a function $\Card:\FinSet\to\NN$
such that $\Card(S)$ is the cardinality of the finite set $S$.\footnote{%
$\Card(S)=n$ is also phrased as: $S$ \emph{is in the same component in $\Set$
as} $\bn{n}$, or \emph{$S$ has cardinality $n$},
or $S$ \emph{is an $n$-element set}.}
\end{definition}

Observe that we have identifications in
$\FinSet_0 \eqto \FinSet_1 \eqto \bn{1} $, and in
$\FinSet \eqto \sum_{n:\NN}\FinSet_n$ by \cref{lem:maxonefinitetype}.
Also, $\FinSet$ is the image of the map $\Fin : \NN \to \UU$
from~\cref{def:finiteset}, and is hence essentially $\UU$-small
(for any universe $\UU$), by~\cref{pri:replacement}, \cref{P1} in
\cref{sec:natural-numbers}, and our assumption
that $\UU_0$ is the smallest universe.

\begin{xca}\label{xca:finsets-decidable}
Show that every finite set is a decidable set.
\end{xca}

We have already seen several examples of 2-element sets:
$\bool$, $\bn{2}$, $\bn{1}\amalg\bn{1}$ that can easily
be identified. Which one to use
depends on the context and is a matter of convenience.
Later we will also use $\set{\pm1}$. In contrast
to these concrete examples, one cannot identify\footnote{%
Any 2-element set is by definition \emph{merely} identified
with $\bn{2}$, but the problem is that we cannot ''name''
the elements, not even one of them. Having a name for one
of the elements would be sufficient, since then the ''other''
element is uniquely determined.}
an \emph{arbitrary} 2-element set with any of these.
The following exercise makes this precise, and gives a
useful and surprising case of a 2-element set
that actually \emph{can} be identified with $\bn{2}$.

\begin{xca}\label{xca:2-element-sets}
Show that $T\eqto T$ is a 2-element set for every 2-element set $T$.
Using univalence, show that $\neg\prod_{T:\FinSet_2}(T\eqto\bn{2})$.
In spite of the above, give an element of
$\prod_{T:\FinSet_2}((T\eqto T)\eqto\bn{2})$.

Finally, give an element of
$\prod_{T:\FinSet_2}(T \eqto (\bn 2\eqto T))$.
\end{xca}

\section{Type families and maps}
\label{sec:typefam}

There is a natural equivalence between maps into a type $A$
and type families parametrized by $A$. The key idea is that the
fibers of a map form a type family. We will elaborate this
idea and some variations.


\begin{lemma}\label{lem:fst-fiber(a)=B(a)}
Let $A:\UU$ and $B:A\to\UU$.
Recall the projection function $\fst: (\sum_{a:A} B(a))\to A$.
The function $e_a: B(a) \to \fst^{-1}(a)$ defined by
$e_a(b)\defeq ((a,b),\refl{a})$ is an equivalence,
for all $a:A$.
\end{lemma}
\begin{proof}
Note that $\fst(x,b)\jdeq x$ and that $a \eqto x$ does
not depend on $b$. Hence
$\fst^{-1}(a) \equivto \sum_{x:A}  (B(x) \times (a \eqto x))$
via rearranging brackets.
Applying \cref{cor:contract-away} leads indeed to
the equivalence $e_a$.
\end{proof}

\begin{lemma}\label{lem:sum-of-fibers}
Let $A,B:\UU$ and $f:A\to B$.
Then $e: \bigl(\sum_{b:B} f^{-1}(b)\bigr)\to A$ defined by
$e(b,a,p)\defeq a$ is an equivalence.
\end{lemma}
\begin{proof}
The function $e$ is the composite of three equivalences
\[
\Bigl(\sum_{b:B} \sum_{a:A} (b\eqto f(a))\Bigr) \equivto
\Bigl(\sum_{a:A} \sum_{b:B} (b\eqto f(a))\Bigr) \equivto
\Bigl(\sum_{a:A} \true\Bigr) \equivto A,
\]
where the first one interchanges the first two arguments, 
the second one contracts away the inner sumtype
(using \cref{lem:thepathspaceiscontractible}), and the third one
is $\fst$ (using \cref{xca:XequivXtimes1}).
\end{proof}

If $f$ in \cref{lem:sum-of-fibers} is an injection, 
then $(\sum_{b:B} f^{-1}(b),\fst)$ corresponds to a subtype of $B$, and hence
$A$ is a $n$-type if $B$ is a $n$-type by \cref{cor:subtype-same-level}.

\begin{lemma}\label{lem:typefamiliesandfibrations}
  Let $A:\UU$ be a type.\footnote{%
    Note that we need $A$ to be in the same universe
    as the one we're taking type families in.}
  Then
  \[
    \preim ~:~ \sum_{B:\UU}(B\to A) \quad\to\quad (A\to\UU)
  \]
  given by $\preim(B,f)(a)\defeq f^{-1}(a)$ is an equivalence.
  The inverse equivalence is given by sending $C:A\to\UU$ to
  $(\sum_{a:A}C(a), \fst)$.
\end{lemma}

\begin{proof}
We apply \cref{lem:weq-iso}, and verify the two conditions.
Let $C:A\to\UU$. We have to identify $C$ with $\preim(\sum_{a:A}C(a), \fst)$.
As $\preim(\sum_{a:A}C(a), \fst)(a)\jdeq \fst^{-1}(a)$, it suffices
by function extensionality to identify the latter fiber with
$C(a)$, for all $a:A$. This follows directly from
\cref{lem:fst-fiber(a)=B(a)} and the univalence axiom.

Let $f: B\to A$.
We have to identify $(\sum_{a:A} f^{-1}(a), \fst)$ with $(B,f)$.
Using the univalence axiom, we get an identification
$\etop{e} : \sum_{a:A} f^{-1}(a) \eqto B$, where $e$ is the equivalence
from \cref{lem:sum-of-fibers}. Using \cref{lem:isEq-pair=},
it remains to give an element of the type
$\pathover{\fst}{(\_)\to A}{\etop{e}}{f}$.

As an auxiliary step we note that for any $p: X \eqto Y$ and $g:X\to A$,
$h:Y\to A$, the type $\pathover{g}{(\_)\to A}{p}{h}$ of paths over $p$
can be identified with the type $g \eqto h\circ{\ptoe{p}}$, since the two
types are equal by definition for $p\jdeq\refl{X}$.
Applying this here means that we must give an identification of
$\fst$ with $f\circ{\ptoe{\etop{e}}}$. Hence it suffices
to identify $\fst$ and $f\circ e$,
which follows by function extensionality from the definition
of $e$ in \cref{lem:sum-of-fibers}.
\end{proof}

The above result can be generalized to situations with more
properties and/or structure. Examples are to be found in
\cref{lem:Prop-Set-pointed-families} below.
We prepare by the following exercises.

\begin{xca}\label{xca:sum-base-path}
Let $X$ and $Y$ be types, $p: Y\eqto X$ an identification,
and $T: X\to\UU$ a type family.
Construct an equivalence of type
$\sum_{x:X} T(x) \equivto \sum_{y:Y} T(\ptoe{p}(y))$.
\end{xca}

\begin{xca}\label{xca:sum-families}
Let $S: \UU\to\UU$ and let $X$ be a type.
Construct an equivalence of type
$(X\to\sum_{Y:\UU} S(Y)) \equivto \sum_{F:X\to\UU}\prod_{x:X}S(F(x))$.
\end{xca}

\begin{construction}\label{lem:Prop-Set-pointed-families}
Let $A$ be a type and $S:\UU\to\UU$.
Then we have equivalences of the following types:
\begin{enumerate}
\item\label{cnstr:families+structure}
$(A\to\sum_{B:\UU}S(B)) \equivto
\sum_{B:\UU}\sum_{f:B\to A}\prod_{a:A}S(\inv f(a))$.
\item\label{lem:Prop-families}
$(A\to\Prop_\UU) \equivto \sum_{B:\UU}\sum_{f:B\to A}
\prod_{a:A}\isprop({f^{-1}(a)})$;
\item\label{lem:Set-families}
$(A\to\Set_\UU) \equivto \sum_{B:\UU}\sum_{f:B\to A}
\prod_{a:A}\isset({f^{-1}(a)})$;
\item\label{cnstr:families+points}
$(A\to\UUp) \equivto \sum_{B:\UU}\sum_{f:B\to A}\prod_{a:A}f^{-1}(a)$.
\end{enumerate}
\end{construction}

\begin{implementation}{lem:Prop-Set-pointed-families}
\ref{cnstr:families+structure}
In view of \cref{xca:sum-families}, and rearranging sums on the right,
it suffices to construct an equivalence of type
$(\sum_{F:A\to\UU}\prod_{a:A}S(F(a))) \equivto
\sum_{(B,f):\sum_{B:\UU}(B\to A)}\prod_{a:A}S(\inv f(a))$.
Now we can apply the equivalence constructed in \cref{xca:sum-base-path}
with $p$ the path induced by the equivalence $\preim$ from
\cref{lem:typefamiliesandfibrations}. Indeed,
for $T(F)\defeq \prod_{a:A}S(F(a))$ we have
$T(\preim(B,f))\jdeq \prod_{a:A}S(\inv f (a))$.

For \ref{lem:Prop-families}, use \ref{cnstr:families+structure}
with $S\defeq \isprop$.

For \ref{lem:Set-families}, use \ref{cnstr:families+structure}
with $S\defeq \isset$.

For \ref{cnstr:families+points}, use \ref{cnstr:families+structure}
with $S\defeq \id_\UU$.
\end{implementation}

Since $\Prop$ is a set, by \cref{lem:Prop-in-Set}, 
we obtain the following corollary
of \cref{lem:Prop-Set-pointed-families}\ref{lem:Prop-families}.
\begin{corollary}\label{cor:Inj(T)-is-set}
  Subtypes as in \cref{def:injtype} correspond to predicates
  by taking fibers, and $\Inj(T)$ is a set, for any type $T$.
\end{corollary}

\begin{xca}
  For any pair of nested universes $\UU:\UU'$,
  let $S : \UU' \to \UU'$ be the predicate that determines the
  essentially $\UU$-small $\UU'$-types,
  \[
    S(A) \defeq \sum_{X:\UU}A\equivto X,
  \]
  as in~\cref{def:ess-loc-small}.
  Show that projection to the $\UU$-type defines an
  equivalence of type $\bigl(\sum_{A:\UU'}S(A)\bigr) \equivto \UU$,
  and whence construct an equivalence of type
  \[
    (A \to \UU) \equivto
    \sum_{B:\UU'}\sum_{f:B\to A}\prod_{a:A}S(\inv f(a)),
  \]
  between families of $\UU$-small types parametrized by $A$
  and maps to $A$ in $\UU'$ with essentially $\UU$-small fibers,
  for any $A:\UU'$.
\end{xca}

\section{Higher truncations}
\label{sec:higher-truncations}

We've seen the propositional truncation in~\cref{sec:prop-trunc} and
the set truncation in~\cref{sec:operations-on-sets}.
As mentioned in~\cref{rem:set-trunc-as-quotient},
it's possible to define the latter in terms of the former by considering
the propositional truncation of the identity types of a type $A$.
In this section we want to generalize this to higher truncation levels
and show how we can inductively define all the $n$-truncation operations
using propositional truncation
combined with the replacement principle, \cref{pri:replacement},
which is used to stay within a given universe.

\begin{construction}\label{def:join-construction-of-truncation}
  For any integer $n\ge-1$ we have an \emph{$n$-truncation operation}
  $\Trunc\blank_n : \UU \to \UU$, along with \emph{unit maps}
  $\trunc\blank_n : A \to \Trunc A_n$, satisfying the following universal property.

  For any $n$-type $B$, precomposition with $\trunc\blank_n$ induces an equivalence:
  \[
    \bigl(\Trunc A_n\to B\bigr) \equivto (A \to B).
  \]
\end{construction}
\begin{implementation}{def:join-construction-of-truncation}
  We proceed by induction.
  For $n\jdeq-1$, we have this from the higher inductive type
  definition, \cref{def:prop-trunc},
  with element constructor $\trunc\blank:A \to \Trunc A$.

  To go from $n$ to $n+1$, we fix a type $A:\UU$ and consider the
  $n$-truncated identity type family
  \[
    I_n : A \to \biggl(A \to \sum_{X:\UU}\mathrm{is}{n}\mathrm{Type}(X)\biggr),
    \quad
    x \mapsto (y \mapsto \Trunc{x\eqto y}_n).
  \]
  Let $\Trunc A_{n+1} \defeq \im(I_n)$ be the image of $I_n$,
  \cref{def:prop-image}, and let $\trunc\blank_{n+1}: A\to\Trunc A_{n+1}$
  be the map from the domain of $I_n$ to its image,
  $x \mapsto (I_n(x),\trunc{(x,\refl{I_n(x)})})$  with
  $I_n(x) \jdeq \Trunc{x\eqto\blank}_n$ as defined above.

  Since the type of $n$-types is an $(n+1)$-type,
  $\Trunc A_{n+1}$ is an $(n+1)$-type by~\cref{lem:level-n-utils}.
  We also note that the map
  \begin{equation}\label{eq:trunc-path-eq}
    \Trunc{x\eqto y}_n \equivto (\trunc x_{n+1} \eqto \trunc y_{n+1}),
  \end{equation}
  induced by the universal property of $n$-truncation,
  is an equivalence.
  Indeed, the right-hand side is equivalent to
  \[
    \prod_{z:A} \bigl(\Trunc{x\eqto z}_n \equivto \Trunc{y\eqto z}_n\bigr),
  \]
  and we get an inverse by going backwards along this equivalence at
  $\trunc{\refl{y}}_n : \Trunc{y\eqto y}_n$.

  To prove the universal property, let $B$ be any $(n+1)$-type
  and $g : A \to B$ any map.

  It suffices to show that for any $z:\Trunc A_{n+1}$,
  there is a contractible type of extensions
  $\sum_{y:B}((\blank\mapsto y)
  \eqto_{(\trunc\blank_{n+1}^{-1}(z))\to B}(g \circ \fst))$,
  visualized by
  \[
    \begin{tikzcd}
      \trunc\blank_{n+1}^{-1}(z) \ar[dr,"g \circ \fst"]\ar[d] & \\
      \bn 1 \ar[r,dashed] & B,
    \end{tikzcd}
  \]
  since then there's a contractible type of extensions of $g$
  to all of $\Trunc A_{n+1}$.
  Since this is a proposition and $\trunc\blank_{n+1}$ is surjective,
  it suffices to prove this for $z$ of the form $\trunc x_{n+1}$ with $x:A$.
  We need to show that the type
  \[
    \prod_{x:A}\sum_{y:B}\prod_{x':A}
    \bigl((\trunc x_{n+1} \eqto \trunc {x'}_{n+1})
    \to (y \eqto g(x'))\bigr)
  \]
  is contractible.
  By the equivalence above, we can rewrite this, first as
  \[
    \prod_{x:A}\sum_{y:B}\prod_{x':A}
    \bigl(\Trunc{x\eqto x'}_n \to (y \eqto g(x'))\bigr),
  \]
  and then, since $y \eqto g(x')$ is an $n$-type, as
  \[
    \prod_{x:A}\sum_{y:B}\prod_{x':A}
    \bigl((x\eqto x') \to (y \eqto g(x'))\bigr).
  \]
  Now we can contract away $x'$ and the identification $x \eqto x'$,
  so we're left with
  \[
    \prod_{x:A}\sum_{y:B}(y \eqto g(x')),
  \]
  which is indeed contractible.

  Finally, we need to re-size $\Trunc A_{n+1}$ to fit in the universe
  $\UU$ that $A$ came from.
  By \eqref{eq:trunc-path-eq}, its identity types are essentially $\UU$-small
  by induction hypothesis, so again since $\trunc\blank_{n+1}$ is a surjection
  from the $\UU$-small type $A$, the replacement principle, \cref{pri:replacement},
  implies that $\Trunc A_{n+1}$ is essentially $\UU$-small.
\end{implementation}
This construction is due to \citeauthor{Rijke-Join}\footcite{Rijke-Join},
see also the presentation in his book\footcite{Rijke-Intro}.

\section{Higher structure: stuff, structure, and properties}
\label{sec:stuff-struct-prop}

Recall from \cref{lem:sum-of-fibers}\marginnote{%
  The precise formalization of the intuitive
  notions of ``stuff'', ``structure'',
  and ``properties'' was worked out
  in terms of category theory in
  \emph{UseNet} discussions between
  John Baez, Toby Bartels, and James Dolan
  on \texttt{sci.physics.research} in 1998.
  It was clear that the simplest description
  was in terms of homotopy types,
  and hence it's even simpler in type theory.
  See also \citeauthor{Baez-Shulman}\footnotemark{}
  for further discussion.}%
\footcitetext{Baez-Shulman}
that any map $f : B \to A$ can be described
as ``projecting away'' its fibers,
by using the equivalence $e$:
\begin{equation}\label{eq:forget-fibers}
  \begin{tikzcd}
    B \ar[rr,"e","\sim"']\ar[dr,"f"'] & &
    \sum_{a:A} \inv f(a)\ar[dl,"\fst"] \\
    & A &
  \end{tikzcd}
\end{equation}
We say that $f$ \emph{forgets} these fibers.\index{forget}
If $A$ and $B$ are groupoids,
these fibers are themselves groupoids,
but it can happen that they are sets, propositions, or even contractible.
Accordingly, we say that:
\begin{itemize}
\item $f$ \emph{forgets at most structure} if all the fibers are sets;%
  \index{forget!structure}
\item $f$ \emph{forgets at most properties} if all the fibers are propositions;%
  \index{forget!properties}
\item $f$ \emph{forgets nothing} if all the fibers are contractible.
\end{itemize}
Here, the structure and properties in question are \emph{on $a$} or \emph{of $a$}, respectively, as captured by the fibers at $a$, for each $a:A$.
Of course, a map forgets properties if and only if
it's an injection,
and it forgets nothing if and only if it's an equivalence.

Going in the other direction,
we say that:
\begin{itemize}
\item $f$ \emph{forgets at most $n$-structure}
  if all the fibers are $n$-truncated.\index{forget!higher structure}
  If $n\ge1$, this is therefore a kind of \emph{higher structure}.\footnote{%
    We're updating the terminology slightly: In the above references,
    $n$-structure is referred to as \emph{$n$-stuff},
    but nowadays the term \emph{higher structure} is more common,
    so we have renamed $n$-stuff into \emph{$n$-structure}.}
\end{itemize}
Thus, an element of a groupoid is $1$-structure
(this is sometimes informally called \emph{stuff}\index{stuff|see{forget!higher structure}}),
while an element of a set is a structure, or $0$-structure,
while an proof of a proposition is a property, or $(-1)$-structure.

Looking at \eqref{eq:forget-fibers} another way,
we see that to give an element $b$ of $B$ lying
over a given element $a:A$ amounts to
specifying an element of $\inv f(a)$,
so we say that the elements of $B$
are elements of $A$ \emph{with extra $n$-structure},
if the fibers $\inv f(a)$ are $n$-truncated.

Refining the usual image and image factorization from
\cref{def:prop-image,xca:unique-fact-image},
using \cref{lem:sum-of-fibers},
we can factor $f : B \to A$ through
first its \emph{$0$-image}
and then its usual $(-1)$-image\index{image} as follows:%
\footnote{Using the general $n$-truncation
  from \cref{sec:higher-truncations},
  we can define the $n$-image
  in a similar way and prove that
  the $n$-image factorization is unique.
  See \cref{sec:higher-images} for the details.
  Since the unit type $\bn 1$ is the unique $(-2)$-type,
  we have $\Trunc{X}_{-2} \eqto \bn 1$ for any type $X$.}
\[
  B \eqto \sum_{a:A} f^{-1}(a) \to
  \sum_{a:A} \Trunc{f^{-1}(a)}_0 \to
  \sum_{a:A} \Trunc{f^{-1}(a)}_{-1} \to A
%  \sum_{a:A} \Trunc{f^{-1}(a)}_{-2} \eqto A. %needed? Overfull line!
\]
Here, the first map \emph{forgets pure higher structure},
the second map \emph{forgets pure structure},
while the last forgets at most properties
(this is the inclusion of the usual image).
Of course, each of these maps may happen to forget nothing at all.
Saying that the second map forgets \emph{pure} structure
indicates that not only are the fibers sets,
they are \emph{nonempty} sets,
so the structure in question exists, at least.
Note also that the fibers of the first map are connected,
which indicates that what is forgotten at this step, if anything,
is pure higher structure.

\begin{example}\label{exa:stuff-struct-prop}
  Let us look at some examples:
  \begin{itemize}
  \item The first projection $\fst : \FinSet \times \FinSet \to \FinSet$
    forgets $1$-structure (stuff), namely the second set in the pair.
  \item The first projection $\fst : \sum_{A:\FinSet} A \to \FinSet$
    from the type of pointed finite sets to the type of finite sets
    forgets structure, namely the structure of a chosen point.
  \item The inclusion of the type of sets with cardinality
    $n$, $\FinSet_n$, into the type of all finite sets, $\FinSet$,
    forgets properties, namely the property
    ``having cardinality $n$''.\qedhere
    \end{itemize}
\end{example}
\begin{xca}\label{xca:stuff-struct-prop}
  Analyze more examples of maps between groupoids
  in terms of ``what is forgotten''.
\end{xca}
\begin{xca}\label{xca:0Im-to-Im}
  Let $\trunc{\_}' : \Trunc{f^{-1}(a)}_0 \to \Trunc{f^{-1}(a)}$ be the
  map defined by the induction principle in \cref{def:set-truncation}
  from $\trunc{\_} : f^{-1}(a) \to \Trunc{f^{-1}(a)}$.
  In the refined image factorization above, the map for the second arrow
  maps any pair $(a,x)$ with $x:\Trunc{f^{-1}(a)}_0$ to the pair $(a,\trunc{x}')$.
  For any $p:\Trunc{f^{-1}(a)}$, give an equivalence from the fiber
  of the latter map at $(a,p)$ to $\Trunc{f^{-1}(a)}_0$.
  What is forgotten by this map, and what is remembered?
\end{xca}


% Local Variables:
% fill-column: 144
% latex-block-names: ("lemma" "theorem" "remark" "definition" "corollary" "fact" "properties" "conjecture" "proof" "question" "proposition" "exercise")
% TeX-master: "book"
% End: