Sum α β, or α ⊕ β, is the disjoint union of types α and β. An element of α ⊕ β is either of the form .inl a where a : α, or .inr b where b : β.

Constructors

inl.{u, v} {α : Type u} {β : Type v} (val : α) : α ⊕ β

inr.{u, v} {α : Type u} {β : Type v} (val : β) : α ⊕ β

PSum α β, or α ⊕' β, is the disjoint union of types α and β. It differs from α ⊕ β 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 True ⊕' Nat.

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. PSum is usually only used in automation that constructs sums of arbitrary types.

Constructors

inl.{u, v} {α : Sort u} {β : Sort v} (val : α) : α ⊕' β

inr.{u, v} {α : Sort u} {β : Sort v} (val : β) : α ⊕' β