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.

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.