I am working my way through the introductory material of Homotopy Type Theory and by the end of section $1.5$ it is clear that I did not have the earlier material down as clearly as I had thought. I had a couple of questions about some notation which seems to be rather significant but I cannot make sense of.
Background: This is my very first look at type theory. I've read the introduction so I have some idea where we're headed but I do not have any clue what use the individual constructions have in the "bigger picture" sense.
The book states that a $\Pi$-type requires a type $A$ and a family of types $A\to\mathcal U$. However, it's then perfectly find writing things like $$\mathrm{swap}:\prod_{A:\mathcal U}\prod_{B:\mathcal U}\prod_{C:\mathcal U} (A\to B\to C)\to (B\to A\to C),$$ which seems to imply that dependent function types are themselves families of types. Am I misinterpreting the use of the triple $\Pi$ here?
Perhaps I am using the wrong language, but $a$ and $b$ in the above example strike me as "bound" variables; I think I mean that it would be valid to apply $\alpha$-conversion to them. If this is true, I find the definition of the recursor a little bit awkward. It is first used in the context of product types, and the book states that $\mathrm{rec}_{A\times B}$ is of type $$\prod_{C:\mathcal U}(A\to B\to C)\to A\times B\to C$$ with defining equation $$\mathrm{rec}_{A\times B}(C,g,(a,b)) :\equiv g(a)(b).$$ What is the $C$ doing in the defining equation? Isn't that variable bound?
Is the intuition behind dependent function types something like a formalization of those "heterogenous functions" that are so common in differential equations— but which I've never seen in any other context— that are like $y(t,x)$ where $x:\Bbb R\to\Bbb R$ is a function dependant on $t$?
Thank you in advance for your time and patience!
Let $T(a)$ be (a formula using $a$ that describes) a type for each $a$, then a habitant of $\prod_{a:A}T(a)$ is a dependent function $\ f$ which is defined on $A$ and satisfies $f(a):T(a)$ for all $a$. So, the notation $$f:\prod_{a:A}T(a)$$ is the generalized version of $f:A\to B$ (where $T(a)=B$ would be for all $a$), that is, type $A$ is the domain of $f$, and we can write down $f(a)$ for any $a:A$.
In the second example above, ${\rm rec}_{A\times B}$ is thus a dependent function from $\mathcal U$, so $\ {\rm rec}_{A\times B}(C)\ $ makes sense and is of type $(A\to B\to C)\to A\times B\to C$.
In the first example, consider the function with $3$ variables $$T(A,B,C):\equiv\ (A\to B\to C)\to (B\to A\to C)$$ this formula defines a type $T(A,B,C):\mathcal U$ for each triple of types $A,B,C:\mathcal U$. (We might also write it using $\lambda A.\lambda B.\lambda C\dots$). So that, by the way, $T:\mathcal U\to\mathcal U\to\mathcal U\to\mathcal U $.
Now, the dependent function $\ {\rm swap}:\displaystyle\prod_{A,B,C:\mathcal U}T(A,B,C)\ $ inputs three types, and $${\rm swap}(A,B,C): (A\to B\to C)\longrightarrow (B\to A\to C) \\ {\rm swap}(A,B,C,f,b,a):\equiv f(a,b)\,:C\,. $$