This brief exposé lays the foundations for studying homotopy type theory; the concepts from here will re-appear in 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, elimination, computation (FIEC).
How to form a new type of this kind. For example
How to construct elements of this kind. For example, a function type has one constructor:
- 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,
is judgmentally equal to the expanded function .
- 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:
The dependent product type (
Instead of defining projections
In order to be able to write dependent functions over the product type, we can define function
To prove a property for all elements of a product, 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:
with the defining equation:
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:
The dependent pair type (
The dependent pair type is written
However, the second projection must be a dependent function, whose type involves the first projection function:
Thus, we need the induction principle for
We can then derive a function:
In order to package up the recursion and induction principles into a recursor for
Now, we present the type-theoretic axiom of choice where
In English, this reads: if
Let's also provide an example of the magma type, in which the second component depends on the first component:
Interlude: Coproduct types and booleans
The recursor for coproduct types can be written as:
The if-then-else pattern in general programming practice utilizes booleans as follows:
and primitive recursion
To define infinite types like
Given step 0, and a next-step function, we can define:
We can generalize general recursion to dependent functions as follows:
with these defining equations:
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
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
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
There is a function:
We can conclude that
If we package up path induction into a single function, it takes the form:
with the equality, traditionally called
Indiscrenability of identicals is an instance of path induction, as we will show later.
By fixing a certain
Since every path is of the form
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
In the homotopy interpretation, type of triples