English
There is a canonical bijection between the W-type WType β and the sigma type Σ a:α, β a → WType β, expressing WType as the fixed point of the polynomial functor X ↦ Σ a:α, β a → X.
Русский
Существует каноническая биекция между W-type и сигма-типом Σ a:α, β a → WType β, показывающая, что WType является фиксированной точкой полиномиального отображения X ↦ Σ a:α, β a → X.
LaTeX
$$$WType(\beta) \cong \Sigma a:\alpha,\; (\beta(a) \to WType(\beta)).$$$
Lean4
/-- The canonical bijection with the sigma type, showing that `WType` is a fixed point of
the polynomial functor `X ↦ Σ a : α, β a → X`. -/
@[simps]
def equivSigma : WType β ≃ Σ a : α, β a → WType β
where
toFun := toSigma
invFun := ofSigma
left_inv := ofSigma_toSigma
right_inv := toSigma_ofSigma
