Relationship between cartesian product and dependent product type

Question

Introduction:

Hi, I'm quite new to types so apologies in advance for the basic question and for any abuse of terminology. I believe I have a critical misunderstanding of dependent product types (and probably about types in general to be quite honest). My questions is based on a reading of Andrej's very helpful answer here.

I see the relationship between dependent sum types and the cartesian product, but I do not see the relationship between dependent product types and the cartesian product.

Question / Ask:

I was wondering if someone could provide a slower, step-by-step walkthrough of how to get to cartesian products from a special case of dependent product types (specifically how we get an ordered tuple from a dependent function).

My Thoughts:

In the first and second paragraphs of Andrej's answer, he relates a binary product to a dependent product type, stating first that we can write a binary product of sets as $\Pi_{i\in I}X_{i}$ and then stating second that we can write a dependent product type as $\Pi(i:I)X(i)$ which can then be used to get a binary product $A \times B$ as a special case if we take $I = \text{Bool}$, $X(\text{false})=A$, and $X(\text{true})=B$.

However, in my head these two $\Pi$ symbols mean something fairly different. In the first ($\Pi_{i\in I}X_{i}$), we are describing a set of ordered tuples $\{(x_1,x_1,\ldots,x_n) \space | \space x_1 \in X_1 , x_2 \in X_2, \ldots, x_n \in X_n\}$ where every combination of $(x_1, x_2, \ldots, x_n)$ is accounted for, whereas in the second ($\Pi(i:I)X(i)$), we are describing the type of a function that maps every element $i : I$ to an element in $X(i)$, where it's not necessarily true that for every $x \in X(i)$ there exists a function $f_x$ such that $f_x(i) = x$. How do we get an ordered tuple from a function?

To add to my confusion, the explanation of dependent product types on ncatlab here explicitly states the following:

It [dependent product types] includes function types as the special case when B is not dependent on A. Note that a binary product type is rather different, being actually a special case of a dependent sum type.

Answer 1

Lets introduce $[n] = \{1,...,n\}$ as a convenience type and look a function $f$ in $\Pi (i:[n]) X(i)$. Now $f[i]$ maps to $x_i \in X_i$. So we could think of $f$ as an ordered sequence/tuple: $f \simeq (x_1,...,x_n)$. Of course for different indexing types its not an ordered tuple in the "classical integer index" sense.

Also $\Pi (i:[n]) X(i)$ contains all of the $n$-long tuples and just some as you thought; so for every $x \in X_i$ there is $f_x: \Pi(i:I)X(i)$ with $f_X(i) = x$.

The last quote is easy to misunderstand; what they try to say is $A \times B = \Sigma (a:A) B $. Where the second object is a dependent sum type $\Sigma (a:A) B(a)$. With $B(a) = B$ constant. I usually think of inhabitants of $\Sigma (a:A) B(a)$ as a pairs $(a, b_a \in B(a))$ and of $\Pi(i:I)X(i)$ as functions $f(i) = x_i \in X_i$. At "runtime" the a function can be evaluated at any $i$ but a pair is fixed.