English
Let α and β be types. The sum α ⊕ β is naturally equivalent to β ⊕ α via swapping the two summands. In particular there exists a bijection between α ⊕ β and β ⊕ α given by inl a ↦ inr a and inr b ↦ inl b.
Русский
Пусть α и β — множества. Сумма α ⊕ β естественно эквивалентна β ⊕ α через обмен местами компонентов. В частности существует биекция между α ⊕ β и β ⊕ α, которая отправляет inl a в inr a и inr b в inl b.
LaTeX
$$$$\alpha \oplus \beta \simeq \beta \oplus \alpha.$$$$
Lean4
/-- Sum of types is commutative up to an equivalence. This is `Sum.swap` as an equivalence. -/
@[simps -fullyApplied apply]
def sumComm (α β) : α ⊕ β ≃ β ⊕ α :=
⟨Sum.swap, Sum.swap, Sum.swap_swap, Sum.swap_swap⟩
