Dependent Sum

Definition

A dependent pair (or dependent sum type) is a generalization of 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

Introduction rule: Given $a:A$ and $b:B(a)$, we can form $(a,b):{\Sigma }_{x:A}B(x)$.

Elimination rule: Given $p:{\Sigma }_{x:A}B(x)$, we have projections:

• ${\pi }_1(p):A$
• ${\pi }_2(p):B({\pi }_1(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$
• 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