Lean4
/-- The functor which deletes the point of a pointed type. In return, this makes the maps partial.
This is the computable part of the equivalence `PartialFunEquivPointed`. -/
@[simps obj map]
def pointedToPartialFun : Pointed.{u} ⥤ PartialFun
where
obj X := { x : X // x ≠ X.point }
map f := PFun.toSubtype _ f.toFun ∘ Subtype.val
map_id _ := PFun.ext fun _ b => PFun.mem_toSubtype_iff (b := b).trans (Subtype.coe_inj.trans Part.mem_some_iff.symm)
map_comp {X Y Z} f
g := by
refine PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ => (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm
suffices c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a) by aesop
rintro rfl
refine ⟨fun h => hc.symm <| g.map_point ▸ congr_arg g.toFun h, hc.symm⟩
