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

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 : α) : α ⊕ β

  Left injection into the sum type α ⊕ β. If a : α then .inl a : α ⊕ β.

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

  Right injection into the sum type α ⊕ β. If b : β then .inr b : α ⊕ β.

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

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 : α) : α ⊕' β

  Left injection into the sum type α ⊕' β. If a : α then .inl a : α ⊕' β.

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

  Right injection into the sum type α ⊕' β. If b : β then .inr b : α ⊕' β.