How is dependent function type for a constant family equal to ordinary function type?

41 Views Asked by At

On page 34 of the Homotopy Type Theory book, they say if $B : A \to \mathcal{U}$ is the constant family $B(x) = B_0$, then $\Pi_{(x:A)}(B(x))$ still takes $x \in A$ into $\mathcal{U}$ namely to the element $B_0$. So how is this pi-type equivalent to $(A \to B)$? Is it a mistake in the book?