Data.Sigma

v11.3.15 • Dependent Pairs

Dependent pairs (Sigma types) where the type of the second component depends on the value of the first.

Types

Sigma :: (A : *) -> (B : A -> *) -> *

The dependent pair type.

Implementation 
data Sigma A B = Sigma (x : A) (B x)

Functions

fst :: Sigma A B -> A

Returns the first component of a dependent pair.

Implementation 
fst p = case p of
    Sigma a b -> a

snd :: (p : Sigma A B) -> B

Returns the second component of a non-dependent pair.

Implementation 
snd p = case p of
    Sigma a b -> b

NOTE: Herman Geuvers showed that dependent eliminator principle is non-derivable in second-order polymorphic lambda calculus.