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 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?

  • 1
    $\begingroup$ Isn't this is in perfect analogy to usual arithmetic? $nm=\sum_{i=1}^mn$, $n^m=\prod_{i=1}^mn$. $\endgroup$ Sep 24, 2014 at 9:29
  • $\begingroup$ The accepted answer is an excellent explanation. I have seen papers that use the notation "dependent function space" and "dependent pair space" instead of "product" and "sum" to avoid this confusion, since the intuition isn't clear if you're not familiar with the underlying theory, particularly for dependently typed programming $\endgroup$ Oct 30, 2021 at 19:20

1 Answer 1


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 $Q(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.

  • $\begingroup$ Typo: should be "Q:A->Type where Q(x) = B for all x:A". $\endgroup$
    – Mike Stay
    Oct 29, 2021 at 15:15
  • $\begingroup$ Thanks, fixed it. You know, you can edit other people's answers around here. $\endgroup$ Oct 29, 2021 at 20:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.