# Relationship between dependent sum type and dependent product type?

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?

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.
1. $$\prod_{n:\mathbb{N}} P(n)$$
2. $$\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)