11.15. Dependent Pairs🔗

Planned Content

Describe Sigma and PSigma, their syntax and API. What is the relationship to Subtype and Exists?

Tracked at issue #176

structure

Sigma.{u, v} {α : Type u} (β : α → Type v)
    : Type (max u v)

Sigma β, also denoted Σ a : α, β a or (a : α) × β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It is sometimes known as the dependent sum type, since it is the type level version of an indexed summation.

Constructor

Sigma.mk.{u, v}

Constructor for a dependent pair. If a : α and b : β a then ⟨a, b⟩ : Sigma β. (This will usually require a type ascription to determine β since it is not determined from a and b alone.)

Fields

fst : α

The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

snd : β self.fst

The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.

structure

PSigma.{u, v} {α : Sort u} (β : α → Sort v)
    : Sort (max (max 1 u) v)

PSigma β, also denoted Σ' a : α, β a or (a : α) ×' β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It differs from Σ a : α, β a in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like (p : Nat) ×' p = p.

The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSigma is usually only used in automation that constructs pairs of arbitrary types.

Constructor

PSigma.mk.{u, v}

Constructor for a dependent pair. If a : α and b : β a then ⟨a, b⟩ : PSigma β. (This will usually require a type ascription to determine β since it is not determined from a and b alone.)

Fields

fst : α

The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

snd : β self.fst

The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.