English
The sum α ⊕ β is equivalent to a Sigma-type over Bool: α ⊕ β ≃ Σ b, bif b then β else α.
Русский
Сумма α ⊕ β эквивалентна сигма-типу над Bool: α ⊕ β ≃ Σ b, bif b then β else α.
LaTeX
$$$$\alpha \oplus \beta \simeq \Sigma b:\mathrm{Bool},\; \text{bif } b \text{ then } \beta \text{ else } \alpha.$$$$
Lean4
/-- `α ⊕ β` is equivalent to a `Sigma`-type over `Bool`. Note that this definition assumes `α` and
`β` to be types from the same universe, so it cannot be used directly to transfer theorems about
sigma types to theorems about sum types. In many cases one can use `ULift` to work around this
difficulty. -/
def sumEquivSigmaBool (α β) : α ⊕ β ≃ Σ b, bif b then β else α :=
⟨fun s => s.elim (fun x => ⟨false, x⟩) fun x => ⟨true, x⟩, fun s =>
match s with
| ⟨false, a⟩ => inl a
| ⟨true, b⟩ => inr b,
fun s => by cases s <;> rfl, fun s => by rcases s with ⟨_ | _, _⟩ <;> rfl⟩
-- See also `Equiv.sigmaPreimageEquiv`.
