Basic concerns about dependent function types 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!
 A: 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\,. $$
