English
There is a canonical equivalence between the W-type constructed from Listβ γ and the ordinary list List γ. Concretely, WType (Listβ γ) is equivalent to List γ via an explicit equivalence with forward map toList and inverse map ofList, together with the standard left and right inverse properties.
Русский
Существует каноническая эквивалентность между W-типа, построенного из Listβ γ, и обычного списка List γ. Конкретно, WType(Listβ γ) эквивалентен List γ через явное соответствие с отображением вперед toList и обратным отображением ofList, обладающим свойствами левой и правой обратности.
LaTeX
$$$\text{WType}(\text{Listβ }\gamma) \simeq \text{List }\gamma$$$
Lean4
/-- Lists are equivalent to their associated `WType` -/
def equivList : WType (Listβ γ) ≃ List γ where
toFun := toList _
invFun := ofList _
left_inv := leftInverse_list _
right_inv := rightInverse_list _
