Sigma.idr

Sigma Types

One of the cornerstones of dependently types programing is Σ-types. They can have many interpretations:

• A dependent pair where the second value’s type depends on the first
• An existential quantifier for a predicate
• The dependent coproduct over indexed types

Definition

A dependent pair is given by a type $a$ and another type $b:a\to Type$ indexed over $a$.

typebind
record Σ (a : Type) (b : a -> Type) where
  constructor (##)
  ||| First projection of sigma
  π1 : a
  ||| Second projection of sigma
  π2 : b π1

Notice the use of the typebind keyword on the record declaration. This allows us to write Σ (n : Nat) | Fin n without having to use a lambda to bind n.

Like before, here is a selection of helper function and properties about Σ-types.

The first fact of note is that Σ-types can define both products and coproducts

Proposition

Products are given by a Σ-type where the second projection does not depend on the first.

Product : Type -> Type -> Type
Product a b = Σ (_ : a) | b

Proposition

Coproducts are given by a Σ-type where the first projection is a choice of type, and the second projection is the type selected.

Coproduct : Type -> Type -> Type
Coproduct a b = Σ (isLeft : Bool) | if isLeft then a else b

• add currying