2
$\begingroup$

I'm trying to understand the connections between a few different concepts fundamental to dependent type theory.

  • Dependent functions ($\Pi$-types)
    • Including non-dependent functions ($A \rightarrow B$)
  • Dependent pairs ($\Sigma$-types)
    • Including non-dependent products ($A \times B$)
  • Coproducts ($A + B$)

Homotopy Type Theory says the following about $\Sigma$s and $\Pi$s:

[ $\Sigma$ ] is called a dependent pair type, or $\Sigma$-type, because in set theory it corresponds to an indexed sum (in the sense of a coproduct or disjoint union) over a given type.

The name "$\Pi$-type" is used because this type can also be regarded as the cartesian product over a given type

(I don't think I fully understand this point)

In a non-dependent setting I'm accustomed to calling coproducts "sums" because the number of inhabitants of a coproduct is the sum of its constituent types' inhabitants - $|A+B| = |A| + |B|$. Likewise I call dependent pairs "products" because $|(A,B)| = |A| \cdot |B|$. Also functions can be called exponentials - $|A \rightarrow B| = |B|^{|A|}$!

Now for the question.

Why does it make sense in Type Theory to use $\Sigma$ for products and $\Pi$ for exponentials? It seems like everything is shifted between non-dependent and dependent types.

  • sums approximately correspond to dependent coproducts
  • products approximately correspond to dependent sums
  • exponentials approximately correspond to dependent products
  • what about dependent exponentials?

What's the deeper connection?

$\endgroup$
  • 1
    $\begingroup$ Isn't this is in perfect analogy to usual arithmetic? $nm=\sum_{i=1}^mn$, $n^m=\prod_{i=1}^mn$. $\endgroup$ – Emil Jeřábek Sep 24 '14 at 9:29
13
$\begingroup$

I think what's confusing you is that $A \times B$ is both a product and a coproduct:

  • It is the product of two factors, namely $A$ and $B$.
  • It is the coproduct of $A$-many copies of $B$.

Once you realize this, you will see that we can obtain $A \times B$ as both a $\sum$ and a $\prod$:

  1. Take $P : \mathtt{bool} \to \mathsf{Type}$ where $P(\mathtt{false}) = A$ and $P(\mathtt{true}) = B$. Then $$\sum_{b : \mathtt{bool}} P(b) \simeq A + B$$ and $$\prod_{b : \mathtt{bool}} P(b) \simeq A \times B$$

  2. Take $Q : A \to \mathsf{Type}$ where $P(x) = B$ for all $x : A$. Then $$\sum_{x : A} Q(x) \simeq A \times B$$ and $$\prod_{x : A} Q(x) \simeq (A \to B)$$

We should therefore not pay attention to $A \times B$ when deciding on a good naming scheme for these two constructs.

The dependent exponential is exactly a dependent product.

$\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.