<p>I think what's confusing you is that <span class="math-container">$A \times B$</span> is <em>both</em> a product and a coproduct:</p>
<ul>
<li>It is the product of two factors, namely <span class="math-container">$A$</span> and <span class="math-container">$B$</span>.</li>
<li>It is the coproduct of <span class="math-container">$A$</span>-many copies of <span class="math-container">$B$</span>.</li>
</ul>
<p>Once you realize this, you will see that we can obtain <span class="math-container">$A \times B$</span> as both a <span class="math-container">$\sum$</span> and a <span class="math-container">$\prod$</span>:</p>
<ol>
<li><p>Take <span class="math-container">$P : \mathtt{bool} \to \mathsf{Type}$</span> where <span class="math-container">$P(\mathtt{false}) = A$</span> and <span class="math-container">$P(\mathtt{true}) = B$</span>. Then
<span class="math-container">$$\sum_{b : \mathtt{bool}} P(b) \simeq A + B$$</span>
and
<span class="math-container">$$\prod_{b : \mathtt{bool}} P(b) \simeq A \times B$$</span></p>
</li>
<li><p>Take <span class="math-container">$Q : A \to \mathsf{Type}$</span> where <span class="math-container">$Q(x) = B$</span> for all <span class="math-container">$x : A$</span>. Then
<span class="math-container">$$\sum_{x : A} Q(x) \simeq A \times B$$</span>
and
<span class="math-container">$$\prod_{x : A} Q(x) \simeq (A \to B)$$</span></p>
</li>
</ol>
<p>We should therefore <em>not</em> pay attention to <span class="math-container">$A \times B$</span> when deciding on a good naming scheme for these two constructs.</p>
<p>The dependent exponential is <em>exactly</em> a dependent product.</p>

CC BY-SA 4.0
2021-10-29T15:15:46.670Z
Typo: should be "Q:A->Type where Q(x) = B for all x:A".
Mike Stay
CC BY-SA 4.0
2021-10-29T20:58:49.453Z
Thanks, fixed it. You know, you can edit other people's answers around here.
Andrej Bauer
CC BY-SA 4.0
2014-09-24T10:20:06.787Z
2021-10-29T20:58:33.390Z
2021-10-29T20:58:33.390Z
Andrej Bauer
<p>I'm trying to understand the connections between a few different concepts fundamental to dependent type theory.</p>
<ul>
<li>Dependent functions (<span class="math-container">$\Pi$</span>-types)
<ul>
<li>Including non-dependent functions (<span class="math-container">$A \rightarrow B$</span>)</li>
</ul>
</li>
<li>Dependent pairs (<span class="math-container">$\Sigma$</span>-types)
<ul>
<li>Including non-dependent products (<span class="math-container">$A \times B$</span>)</li>
</ul>
</li>
<li>Coproducts (<span class="math-container">$A + B$</span>)</li>
</ul>
<p><em>Homotopy Type Theory</em> says the following about <span class="math-container">$\Sigma$</span>s and <span class="math-container">$\Pi$</span>s:</p>
<blockquote>
<p>[ <span class="math-container">$\Sigma$</span> ] is called a <strong>dependent pair type</strong>, or <span class="math-container">$\Sigma$</span>-<strong>type</strong>, because in set theory it corresponds to an indexed sum (in the sense of a coproduct or disjoint union) over a given type.</p>
<p>The name &quot;<span class="math-container">$\Pi$</span>-type&quot; is used because this type can also be regarded as the cartesian product over a given type</p>
</blockquote>
<p>(I don't think I fully understand this point)</p>
<p>In a non-dependent setting I'm accustomed to calling coproducts &quot;sums&quot; because the number of inhabitants of a coproduct is the sum of its constituent types' inhabitants - <span class="math-container">$|A+B| = |A| + |B|$</span>. Likewise I call pairs &quot;products&quot; because <span class="math-container">$|(A,B)| = |A| \cdot |B|$</span>. Also functions can be called exponentials - <span class="math-container">$|A \rightarrow B| = |B|^{|A|}$</span>!</p>
<p>Now for the question.</p>
<p>Why does it make sense in Type Theory to use <span class="math-container">$\Sigma$</span> for products and <span class="math-container">$\Pi$</span> for exponentials? It seems like everything is shifted between non-dependent and dependent types.</p>
<ul>
<li>sums approximately correspond to dependent coproducts</li>
<li>products approximately correspond to dependent sums</li>
<li>exponentials approximately correspond to dependent products</li>
<li>what about dependent exponentials?</li>
</ul>
<p>What's the deeper connection?</p>

CC BY-SA 3.0
2014-09-24T09:29:12.807Z
Isn't this is in perfect analogy to usual arithmetic? $nm=\sum_{i=1}^mn$, $n^m=\prod_{i=1}^mn$.
Emil Jeřábek
CC BY-SA 4.0
2021-10-30T19:20:50.527Z
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*
Joey Eremondi
<type-theory><dependent-type>
Dependent Sums and Products
Joel Burget
# Dependent Sums and Products

(Asked by: username_0 on 2014-09-24)

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?

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: Isn't this is in perfect analogy to usual arithmetic? $nm=\sum_{i=1}^mn$, $n^m=\prod_{i=1}^mn$.  
> **username_2**: 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*  

---

## 1 answers

### Answer by username_3 on 2014-09-24. Score: 18 | Accepted answer

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.

> **Comments:**
> **username_4**: Typo: should be "Q:A->Type where Q(x) = B for all x:A".  
> **username_3**: Thanks, fixed it. You know, you can edit other people's answers around here.  

---

