Lean4
/-- The functor which maps undefined values to a new point. This makes the maps total and creates
pointed types. This is the noncomputable part of the equivalence `PartialFunEquivPointed`. It can't
be computable because `= Option.none` is decidable while the domain of a general `Part` isn't. -/
@[simps obj map]
noncomputable def partialFunToPointed : PartialFun ⥤ Pointed := by
classical
exact
{ obj := fun X => ⟨Option X, none⟩
map := fun f => ⟨Option.elim' none fun a => (f a).toOption, rfl⟩
map_id := fun X =>
Pointed.Hom.ext <|
funext fun o =>
Option.recOn o rfl fun a =>
(by
dsimp [CategoryStruct.id]
convert Part.some_toOption a)
map_comp := fun f g =>
Pointed.Hom.ext <|
funext fun o =>
Option.recOn o rfl fun a => by
dsimp [CategoryStruct.comp]
rw [Part.bind_toOption g (f a), Option.elim'_eq_elim] }
