I've been reading the Homotopy Type Theory Book, and in the first section is lists out all the kinds of types (function, pair, dependent function …).
Each time that it mentions a new type, it presents a function called the "recursor." For example, the recursor for the unit type is:
$rec_1 : \Pi_{C:U} C \to 1 \to C $ where $rec_1(C,c,*) : \equiv c$
But what is a recursor in general? The book gives a function that has something to do with each type it introduces and calls it the recursor, but what makes it different from any function that can be defined?
Best Answer
It actually doesn't give a recursor for every type it introduces, and particularly not for two of the types you mention. In particular, functions and dependent functions. Another exception is the universes. However, it does for every other type. This is because all the other types are special cases of inductive types (or, later on, higher inductive types).
Quoting the first sentence of section 5.6:
The "et cetera" does not include dependent functions or universes. This section in particular and that chapter in general go into more detail of what a "recursor" is. The short answer is that a recursor, or rather the more general dependent eliminator, is what shows that an inductive type is defined "uniquely" in terms of its constructors.
For the traditional example of an inductive type, the natural numbers, it is not enough to merely state that there is a natural number of called $0$, and for every natural number $n$, another natural number called $\mathsf{succ}(n)$. We need something that states "and nothing else is a natural number". This is what the dependent eliminator does. For $\mathbb N$, the dependent eliminator corresponds to the traditional (second-order) induction principle. The dependent eliminator in this case, i.e. the traditional induction principle, states that if a "predicate" holds for $0$ and for each $n:\mathbb N$ the same "predicate" holds for $\mathsf{succ}(n)$ whenever it holds for $n$, then the "predicate" holds for all $n:\mathbb N$. In other words, we only need to consider these two cases to cover all cases.
With non-trivial inductive families there are some subtleties to this, most notably in the identity type case. These subtleties are arguably the launching point for the whole program of homotopy type theory.