# Documentation

Mathlib.Data.Sigma.Basic

# 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 ι with exactly two elements (see Equiv.sumEquivSigmaBool).

Σ 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.