# Relationship between cartesian product and dependent product type

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.

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.

• The nLab page was badly worded; I've amended it. The binary product type is a special case of both a dependent sum type and a dependent product type, specialised in two different ways. Jul 11, 2022 at 23:26

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.