Dependent Types: How is the dependent pair type analogous to a disjoint union?

The confusion arises from using similar terminology for the structure of a Σ type and for how its values look like.

A value of Σ(x:A) B(x) is a pair (a,b) where a∈A and b∈B(a). The type of the second element depends on the value of the first one.

If we look at the structure of Σ(x:A) B(x), it’s a disjoint union (coproduct) of B(x) for all possible x∈A.

If B(x) is constant (independent of x) then Σ(x:A) B will be just |A| copies of B, that is A⨯B (a product of 2 types).


If we look at the structure of Π(x:A) B(x), it’s a product of B(x) for all possible x∈A. Its values could be viewed as |A|-tuples where a-th component is of type B(a).

If B(x) is constant (independent of x) then Π(x:A) B will be just A→B – functions from A to B, that is Bᴬ (B to A) using the set-theory notation – the product of |A| copies of B.


So Σ(x∈A) B(x) is a |A|-ary coproduct indexed by the elements of A, while Π(x∈A) B(x) is a |A|-ary product indexed by the elements of A.

Leave a Comment