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?


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) $.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.