English
The constructor-type Natα is equivalent to the two-point type PUnit ⊕ PUnit, i.e., Natα has exactly two constructors corresponding to zero and succ.
Русский
Тип Natα эквивалентен двумточечному типу PUnit ⊕ PUnit: у Natα ровно два конструктора, соответствующих нулю и следущему.
LaTeX
$$$$\mathrm{Nat\alpha} \simeq PUnit \oplus PUnit.$$$$
Lean4
/-- `WType.Natα` is equivalent to `PUnit ⊕ PUnit`.
This is useful when considering the associated polynomial endofunctor.
-/
@[simps]
def NatαEquivPUnitSumPUnit : Natα ≃ PUnit.{u + 1} ⊕ PUnit
where
toFun
c :=
match c with
| Natα.zero => inl unit
| Natα.succ => inr unit
invFun
b :=
match b with
| inl _ => Natα.zero
| inr _ => Natα.succ
left_inv
c :=
match c with
| Natα.zero => rfl
| Natα.succ => rfl
right_inv
b :=
match b with
| inl _ => rfl
| inr _ => rfl
