A Lean Companion to Conceptual Mathematics

Session 20: Points of an object🔗

Definition: Point (p. 232)

A point of X is a map {T \rightarrow X} where T is terminal.

See the earlier definition of point on p. 214 (and also cf. the definition of points in sets on p. 19).