Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Hmm… that’s true, given that our page pointed object is all about objects pointed by a map from the terminal object. But there’s certainly a sense in which an object equipped with a map from the unit object is also “pointed”. Maybe “monoidally pointed”?
I made a related comment in the discussion page for pointed object, that there are more general notions of pointing out there, involving maps out of the monoidal unit, which specialize to maps out of the terminal object when interpreted in the doctrine of cartesian monoidal categories. The article pointed object is essentially about that specialization (even though you don’t need all finite products to state the definition).
added pointer to:
for an original use of the terminology
(incidentally, another good example for why it’s a bad idea to denote terminal objects by “$1$”)
Changed the wording a bit, so as to link more smoothly with the new article pointed object in a monoidal category.
1 to 8 of 8