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