English
Let C be a category. There is a canonical equivalence of types between the type Option(C) and WithInitial(C); it sends some a to the object of C inserted by the initial construction, and none to the distinguished initial object star. The inverse sends star back to none and of a back to some a.
Русский
Пусть C — категория. Существуют канонические эквивалентности типов между типами Option(C) и WithInitial(C); отображение отправляет some(a) в соответствующий элемент WithInitial, а none — в начальный объект star. Обратное отображение отправляет star в none, а of(a) — в some(a).
LaTeX
$$$\mathrm{Option}(C) \simeq \mathrm{WithInitial}(C)$$$
Lean4
/-- The equivalence between `Option C` and `WithInitial C` (they are both the
type `C` plus an extra object `none` or `star`). -/
def optionEquiv : Option C ≃ WithInitial C
where
toFun
| some a => of a
| none => star
invFun
| of a => some a
| star => none
left_inv a := by cases a <;> simp
right_inv a := by cases a <;> simp
