2
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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):

  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)
$\endgroup$

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.