I'm reading HoTT book and I'm not sure if I really understand how the recursor function is related to the induction function. It is stated that product types are said to be :
a degenerate example of a general framework for inductive types
Thus, I think the recursor function for product types is a particular case of the induction function for product types : $$rec_{A \times B} : \prod_{C : \mathcal{U}}(A \rightarrow B \rightarrow C) \rightarrow A \times B \rightarrow C$$
$$ind_{A \times B} : \prod_{C : A \times B \rightarrow \mathcal{U}} \left( \prod_{(x: A)} \prod_{(y : B)} C((x,y)) \right) \rightarrow \prod_{x : A \times B} C(x)$$
Am I right by considering the recursor function as the induction function with C not being dependent of A and B ?
Also, this is my first post on this website, please tell me whether I have to rephrase something in a particular way.
Best Answer
Yes, you're correct. The recursor is like the induction principle, but with a less informative type. (Or, the induction principle is recursion with a more informative type.)