Dependent Sum

Definition

A dependent pair (or dependent sum type) is a generalization of the (simple) product type where the type of the second component may depend on the value of the first component.

The dependent pair type is written ${\Sigma }_{x:A}B(x)$ or $\Sigma x:A.B(x)$, where $A$ is a type and $B:A\to \mathcal{U}$ is a type family indexed by $A$.

An element of ${\Sigma }_{x:A}B(x)$ is a pair $(a,b)$ where $a:A$ and $b:B(a)$.

Type Rules

Formation Rule

$$\frac{\Gamma ⊢A:\mathcal{U}\Gamma ,x:A⊢B(x):\mathcal{U}}{\Gamma ⊢{\Sigma }_{x:A}B(x):\mathcal{U}}$$

Introduction Rule

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:B(a)}{\Gamma ⊢(a,b):{\Sigma }_{x:A}B(x)}$$

Elimination Rules

$$\frac{\Gamma ⊢p:{\Sigma }_{x:A}B(x)}{\Gamma ⊢{\pi }_1(p):A}\frac{\Gamma ⊢p:{\Sigma }_{x:A}B(x)}{\Gamma ⊢{\pi }_2(p):B({\pi }_1(p))}$$

$\beta$-Rules

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:B(a)}{\Gamma ⊢{\pi }_1(a,b)\equiv a:A}\frac{\Gamma ⊢a:A\Gamma ⊢b:B(a)}{\Gamma ⊢{\pi }_2(a,b)\equiv b:B(a)}$$

η-Rule

$$\frac{\Gamma ⊢p:{\Sigma }_{x:A}B(x)}{\Gamma ⊢p=({\pi }_1(p),{\pi }_2(p))}$$

Examples

• A vector with length: ${\Sigma }_{n:\mathbb{N}}\text{Vec}(n)$ pairs a natural number with a vector of that length
• Subtypes: ${\Sigma }_{x:A}P(x)$ represents elements of $A$ satisfying predicate $P$ with $\mathrm{isProp}(P(x))(\forall x)$
• Existential quantification: The proposition $\exists x:A.P(x)$ corresponds to ${\Sigma }_{x:A}P(x)$

Special Cases

When $B$ is a constant type family (does not depend on $x$), the dependent pair reduces to the ordinary product type: ${\Sigma }_{x:A}B\cong A\times B$.

Related Concepts

• Product Type: The non-dependent special case
• Ordered Tuple: Concrete elements of product types
• Dependent Product: The dual construction where functions have dependent codomains
• Sum Type: The coproduct, dual to the product