English
There is a natural equivalence between Listα γ and the sum type PUnit ⊕ γ, given by mapping nil to the left unit and cons x to the right element, with an inverse that ignores the left side and reconstructs the list from the right side.
Русский
Существует естественная эквивалентность между Listα γ и суммой типов PUnit ⊕ γ, заданная отображением nil ↦.inl unit и конс x ↦.inr x, с обратным отображением, игнорирующим левую часть и восстанавливающим список из правой части.
LaTeX
$$$\text{Listα }\gamma \simeq PUnit \oplus \gamma$$$
Lean4
/-- `WType.Listα` is equivalent to `γ` with an extra point.
This is useful when considering the associated polynomial endofunctor
-/
def ListαEquivPUnitSum : Listα γ ≃ PUnit.{v + 1} ⊕ γ
where
toFun
c :=
match c with
| Listα.nil => Sum.inl PUnit.unit
| Listα.cons x => Sum.inr x
invFun := Sum.elim (fun _ ↦ Listα.nil) Listα.cons
left_inv
c :=
match c with
| Listα.nil => rfl
| Listα.cons _ => rfl
right_inv
x :=
match x with
| Sum.inl PUnit.unit => rfl
| Sum.inr _ => rfl
