PointedType

Stream: lean4

[Reid Barton]

rss-bot said:

feat: define PointedType as { α : Type u // Nonempty α }
feat: define PointedType as { α : Type u // Nonempty α }
https://github.com/leanprover/lean4/commit/e3241e82bce83048accbbb2eac3f281a7e74b5d7

Could we rename PointedType to something like NonemptyType? In math, "pointed type" (or set) specifically means a type (set) with a distinguished element, not just a nonempty set.

[Kevin Buzzard]

(and a map of pointed types would be expected to take the point to the point)

[Marcus Rossel]

I've never heard of pointed types, but doesn't the Lean definition seem to match this and this description?

[Kevin Buzzard]

No; this is exactly the point. A pointed type is equipped with a special point, it's more like has_zero than Nonempty. The term is used in mathematics to mean constructive nonemptiness, i.e. data rather than a Prop.

[Eric Rodriguez]

mathematicians whenever they are talking about a "pointed" object very much care about said point; it can be the basepoint of the loop or such like but it's never really an "arbitrary" point, it has importance in the theory