Sigma types #
This file proves basic results about sigma types.
A sigma type is a dependent pair type. Like
α × β but where the type of the second component
depends on the first component. More precisely, given
β : ι → Type*,
Sigma β is made of stuff
which is of type
β i for some
i : ι, so the sigma type is a disjoint union of types.
For example, the sum type
X ⊕ Y can be emulated using a sigma type, by taking
exactly two elements (see
Σ x, A x is notation for
Sigma A (note that this is
\Sigma, not the sum operator
Σ x y z ..., A x y z ... is notation for
Σ x, Σ y, Σ z, ..., A x y z .... Here we have
α : Type*,
β : α → Type*,
γ : Π a : α, β a → Type*, ...,
A : Π (a : α) (b : β a) (c : γ a b) ..., Type* with
x : α
y : β x,
z : γ x y, ...
The definition of
Sigma takes values in
Type*. This effectively forbids
Prop- valued sigma
types. To that effect, we have
PSigma, which takes value in
Sort* and carries a more
complicated universe signature as a consequence.