This brief exposé lays the foundations for studying homotopy type theory; the concepts from here will re-appear in [HoTT/2](/HoTT/2), with fresh interpretations. It corresponds exactly to Ch.1 of the HoTT book.

To specify a new type in HoTT, we need to specify four different rules: formation, introduction, elimintion, computation (FIEC).

- How to form a new type of this kind. For example $\Pi_{(x : A)} B(x)$
- How to construct elements of this kind. For example, a function type has one constructor: $f(x) :\equiv 2x$.
- How to use elements of this type. These are called eliminators or `elimination rules`. For instance, a function type has one eliminator, namely function application.
- How the eliminator acts on the constructor. For example, $(\lambda x . \phi)(a)$ is judgementally equal to the expanded function $\lambda f . f(x)$.
- An optional uniqueness principle which expresses uniqueness into or out of the type. Every element of the type is uniquely determined by results of applying type eliminators to it. It is often a provable propositional equality: in this case, we call it `propositional uniqueness principle`.

Broadly speaking, there are two kinds of types: $\Pi$ (which turns out to be a degenerate case of an inductive type, which we will see later) and $\Sigma$.

## The dependent product type ($\Pi$-type)

Instead of defining projections $pr1$ and $pr2$ for the two projections from the pair, we will define a "recursor" as follows:

$$ rec_{A \times B} : \Pi_{C : \mathscr{U}} (A \times B \times C) \rightarrow A \times B \rightarrow C \\ rec_{A \times B}(C, g, (a, b)) :\equiv g(a)(b) $$

So that:

$$ pr1 :\equiv rec_{A \times B}(A, \lambda a . \lambda b . a) \\ pr2 :\equiv rec_{A \times B}(B, \lambda a . \lambda b . b) $$

In order to be able to write dependent functions over the product type, we can define function $f : \Pi_{x : A \times B} C(x)$ by providing $g : \Pi_{x : A} \Pi_{x : B} C((x, y))$ with the defining equation $f((x, y)) = g(x)(y)$.

To prove a property for all elements of a prduct, it is enough to prove it for its canonical elements (the ordered pairs). In the universal case, we call the resulting function induction for product types:

$$ ind_{A \times B} : \Pi_{C : A \times B \rightarrow U} (\Pi_{x : A}\Pi_{y : B} C((x, y))) \rightarrow \Pi_{x : A \rightarrow B} C(x) $$

with the defining equation:

$$ ind_{A \times B}(C, g, (a, b)) :\equiv g(a)(b) $$

Because induction describes how to use an element of the product type, induction is often called the `dependent eliminator`; recursion is called the `non-dependent eliminator`.

Comment: the induction for the unit type turns out to be more useful than the recursor:

$$ uniq_1 : \Pi_{x : \mathbf{1}} x = \star \\ uniq_1(x) :\equiv refl_\star $$

## The dependent pair type ($\Sigma$-type)

The dependent pair type is written $\Sigma_{x : A}, B(x)$. When the second component doesn't depend on the first, we get the cartesian product type $A \times B$. The first projection follows a straightforward extraction:

$$ pr1 : (\Sigma_{x : A} B(x)) \rightarrow A $$

However, the second projection must be a dependent function, whose type involves the first projection function:

$$ pr2 : \Pi_{p: \Sigma_{x : A} B(x)} B(pr1(p)) $$

Thus, we need the induction principle for $\Sigma$-types (the `dependent eliminator`):

$$ g : \Pi_{a : A}\Pi_{b : B(a)} C((a, b)) $$

We can then derive a function:

$$ f : \Pi_{p:\Sigma_{x : A}, B(x)} C(p) $$

In order to package up the recursion and induction principles into a recursor for $\Sigma$, which we will not bother elaborating here. As usual, the recursor is the special case of induction when the family $C$ is fixed.

Now, we present the `type-theoretic axiom of choice` where $R : A \rightarrow B \rightarrow U$:

$$ ac : (\Pi_{a : A} \Sigma_{y : B} R(x, y)) \rightarrow (\Sigma_{f : A \rightarrow B} \Pi_{x : A} R(x, f(x))) \\ ac(g) :\equiv (\lambda x . pr_1(g(x)), \lambda x . pr2(g(x)) \\ \lambda x . pr_1(g(x)) : A \rightarrow B \\ \lambda x . pr_2(g(x)) : \Pi_{x : A} R(x, pr_1(g(x))) $$

In English, this reads: if $\forall x : A$, there is a $y : B$ such that $R(x, y)$, then $\exists f : A \rightarrow B$ such that $\forall x : A$, we have $R(x, f(x))$. We will provide a more familar axiom of choice later.

Let's also provide an example of the magma type, in which the second component depends on the first component:

$$ Magma :\equiv \Sigma_{A : \mathscr{U}} A \rightarrow A \rightarrow A $$

## Interlude: Coproduct types and booleans

The recursor for coproduct types can be written as:

$$ rec_{A + B} : \Pi_{C : \mathscr{U}} (A \rightarrow C) \rightarrow (B \rightarrow C) \rightarrow A + B \rightarrow C \\ rec_{A + B}(C, g_0, g_1, inl(a)) :\equiv g_0(a) \\ rec_{A + B}(\Pi_{C : \mathscr{U}} (C, g_0, g_1, inr(a)) :\equiv g_1(a) $$

The if-then-else pattern in general programming practice utilizes booleans as follows:

$$ rec_2 : \Pi_{C : \mathscr{U}} C \rightarrow C \rightarrow \mathbf{2} \rightarrow C \\ rec_2(C, c_0, c_1, 0_\mathbb{2}) :\equiv c_0 \\ rec_2(C, c_0, c_1, 1_\mathbb{2}) :\equiv c_1 $$

## $\mathbb{N}$ and primitive recursion

To define infinite types like $\mathbb{N}$, we need the additional concept of well-founded recursion. We can package the recursor into a single function, as previously:

$$ rec_\mathbb{N} : \Pi_{C : \mathscr{U}} C \rightarrow (\mathbb{N} \rightarrow C \rightarrow C) \rightarrow \mathbb{N} \rightarrow C $$

Given step 0, and a next-step function, we can define:

$$ rec_{\mathbb{N}}(C, c_0, c_s, 0) = c_0 \\ rec_{\mathbb{N}}(C, c_0, c_s, succ(n)) = c_s(n, rec_\mathbb{N}(C, c_0, c_s, n)) $$

We can generalize general recursion to dependent functions as follows:

$$ ind_{\mathbb{N}} : \Pi_{C : \mathbb{N} \rightarrow U} C(0) \rightarrow (\Pi_{n : \mathbb{N}} C(n) \rightarrow C(succ(n))) \rightarrow \Pi_{n \in \mathbb{N}} C(n) $$

with these defining equations:

$$ f(0) :\equiv c_0 \\ f(succ(n)) :\equiv c_s(n, f(n)) $$

## Identity types

The cornerstone of homotopy type theory is that there can be more than one witness that two objects are equal. These correspond to paths or equivalences in the given space.

The identity family takes two copies of $A$, and illustrates an equality between them: $id_A : A \rightarrow A \rightarrow \mathscr{U}$. The formation rule says that given a type $A : \mathscr{U}$ and two elements $a, b : A$, we can form the type $(a =_A b) : \mathscr{U}$ in the same universe. The introduction rule is a dependent function called reflexivity:

$$ \texttt{refl} : \Pi_{a : A} a = a $$

The elimination rule for identity types is subtle. We begin by considering the consequence that equals may be substituted for equals, called `indiscrenability of identicals`. For every family $C : A \rightarrow \mathscr{U}$, there is a function

$$ f : \Pi_{x, y : A} \Pi_{x =_A y} C(x) \rightarrow C(y) $$

such that:

$$ f(x, x, \texttt{refl}_x) :\equiv id_{C(x)} $$

## Path induction

The induction principle for the identity type is called `path induction`. It can be seen as stating that the family of identity types is freely generated by elements of the form $\texttt{refl}_x : x = x$.

Given functions:

$$ C : \Pi_{x, y : A} (x =_A y) \rightarrow \mathscr{U} \\ c : \Pi_{x : A} C(x, x, \texttt{refl}_x) $$

There is a function:

$$ f : \Pi_{x, y : A} \Pi_{p : x =_A y} C(x, y, p) $$

such that

$$ f(x, x, \texttt{refl}_x) :\equiv c(x) $$

We can conclude that $C(x, y)$ is a reflexive relation that holds whenever $x = y$.

If we package up path induction into a single function, it takes the form:

$$ ind_{=A} : \Pi_{C : \Pi_{x, y : A} (x =_A y) \rightarrow \mathscr{U}} (\Pi_{x : A} C(x, x, \texttt{refl}_x)) \rightarrow \Pi_{x, y : A} \Pi_{p : x =_A y} C(x, y, p) $$

with the equality, traditionally called $J$:

$$ ind_{=A}(C, c, x, x, \texttt{refl}_x) :\equiv c(x) $$

Indiscrenability of identicals is an instance of path induction, as we will show later.

By fixing a certain $a : A$, we can show `based path induction`, a simpler version:

$$ ind'_{=A} : \Pi_{a : A}\Pi_{C : \Pi_{a : A} (a =_A x) \rightarrow \mathscr{U}} C(a, \texttt{refl}_a) \rightarrow \Pi_{x : A} \Pi_{p : a =_A x} C(x, p) $$

Since every path is of the form $\texttt{refl}_a$, if we prove a property for reflexivity paths, then we have provided it for all paths.

Now, we must resolve a question: how can there be many different elements of the identity type (different paths), but also have an induction principle asserting that the only path is reflexivity? It is not that the identity type that is inductively defined; rather, it is the inductive family. In particular, path induction says that the family of types $x =_A y$, as $x$ and $y$ vary over all elements of $A$, inductively defined by the elements of the form $\texttt{refl}_x$. This means that to give an element of any other family, it suffices to consider the cases of the form $(x, y, p)$ dependent on a generic element $(x, y, p)$ of the identity family, it suffices to consider the cases of the form $(x, x, \texttt{refl}_x)$.

In the homotopy interpretation, type of triples $(x, y, p)$, where $x, y$ are endpoints of the path $p$ (in other words, $\Sigma_{x, y : A} (x = y)$), is inductively generated by the constant loops at each point $x$. We will consequently see that that the space corresponding to $\Sigma_{x, y : A} (x = y)$ is a `free path space`. To conclude, $\Sigma_{y : A} (a = y)$ can be regarded as the type of all elements of $A$ which are equal to $a$.