Since dependent sum type ($\sum_{n\in \mathbb{N}} P(n) $) is interpreted as ($\exists n\in \mathbb{N}:P(n) $) and dependent product type ($\prod_{n\in \mathbb{N}} P(n)$) is interpreted as ($\forall n\in \mathbb{N}:P(n)$), is it correct to say that an element of dependent product type represents a set(in a vague way) of elements of corresponding dependent sum type for every n?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
I believe you meaning the following.
A value of type $\prod_{n : \mathbb{N}} P(n)$ is a function which takes a value $n$ of type $\mathbb{N}$ as input and outputs a value of type $P(n)$. So the domain of such a function is $\mathbb{N}$. What is its codomain? Well, the type of the result depends on the value of the input, which is why it's called a dependent product. So it doesn't really have a codomain in the traditional sense.
But we can also view this situation as follows: Yes, such a function $f$ has a codomain, namely the dependent sum $\sum_{m : \mathbb{N}} P(m)$; but with the condition imposed that $(\mathsf{fst} \circ f)(n) = n$ for all $n : \mathbb{N}$, where $\mathsf{fst} : \sum_{m : \mathbb{N}} P(m) \to \mathbb{N}$ is the first projection.
More precisely, the following types are indeed equivalent ("equivalent" as in the HoTT book):
- $\prod_{n:\mathbb{N}} P(n)$
- $\prod_{f : (\mathbb{N} \to (\sum_{m : \mathbb{N}} P(m)))} \prod_{n:\mathbb{N}} ((\mathsf{fst} \circ f)(n) = n)$ (the type of functions satisfying the stated condition)
