sigmatypen

Sigmatypen, or Sigma types, are a kind of dependent pair type in type theory, also called dependent sums. Given a type A and a family of types B(x) indexed by x:A, the Sigma type Σ x:A. B(x) consists of pairs (a, b) where a:A and b:B(a).

Formation rules state that if A is a type and for each a:A the type B(a) is defined, then Σ x:A. B(x) is itself a type. Introduction is provided by the pair constructor (a, b), with a:A and b:B(a). Elimination is handled by projection functions: π1: Σ x:A. B(x) → A and π2: Σ x:A. B(x) → B(π1(s)), where s is an element of the Sigma type.

In programming terms, Sigma types can be deconstructed through pattern matching, allowing access to the first component and the dependent second component. Semantically, they generalize Cartesian products: if B is constant B0, then Σ x:A. B0 is isomorphic to A × B0.

Sigma types are used to encode values together with a witness or proof that depends on the first component, such as a value a:A paired with a proof P(a). They are central in dependently typed languages and proof assistants, including Coq, Agda, and Idris. Notation typically appears as Σ x:A. B(x).

Related concepts include dependent types and dependent function types (Pi types). Sigma types provide a constructive way to form pairs whose second component may vary with the first, enabling precise encoding of data with context-dependent properties.