I was reading the book "Homotopy Type Theory", and got confused about the distinction between a family of types $B : A \to \mathcal U$ and a dependent function type $\Pi_{(x:A)} B(x) : \to \mathcal U $. From the book,
Given a type $A : \mathcal U$ and a family $B : A \to \mathcal U$, we may
construct the type of dependent functions $\Pi_{(x:A)} B(x) : \mathcal U $. There are many alternative notations for this type …
, where the family of types $B : A \to \mathcal U$ is just a function
whose codmain is an universe
But I don't see any construction introduced, just a new notation $\Pi_{(x:A)} B(x) : \mathcal U $. What is the actual construction, and how is the construction different from that of the type family $B: A \to \mathcal U$ itself?
More specifically, given a dependent function $f (x:A) :\equiv \Phi$, which takes an $x:A$ and returns a value in $B(x)$, shouldn't the type of $f$ be $B$, which being a function by definition, does exactly taking $x$ to $B(x)$ (, or $ x \mapsto B(x) \equiv B $)? What's the new notation about?
Best Answer
A type family $ B : A \to \mathcal U $ is a map from the inhabitants of type $ A $ to a type.
However a dependent function $ \Pi_{(x:A)} B(x) $ maps from an inhabitant of $ A$ to an inhabitant within type $ B(x) $. So the inhabitant's type can change depending on the argument.
For example you could have the type family $ \mathcal V : \mathbb{N} \to \mathcal U $. Where $ \mathcal V(x) $ is a type inhabited by natural numbers less than $x$.
You could then have a dependent function $ max : \Pi_{n:\mathbb{N}} \mathcal V(n) $ which returned the largest inhabitant of $ \mathcal V(n) $.
In this example $ max(1) $ would return $ 0 : \mathcal V(1) $.