Hacker News Reader

Comment by pizza | Hacker News Reader

> A set has the least structure. It's a discrete category, with no morphisms other than identities. Conversely, the category of sets has the most structure, since its morphisms don't have to preserve any structure.

https://twitter.com/BartoszMilewski/status/16743572724981104...

View on HN

This is incorrect. The number of morphisms is not what makes mathematical objects more or less structured. What is correct is that the category of sets does not have constraints for morphisms between its objects. Bartosz is equating morphisms and "structure" which is not how most mathematicians think of what it means for a category or an object to be structured.

It seems incorrect to state that his perspective is categorically incorrect. The term “structure” lacks a precise definition and his interpretation isn’t completely invalid.

He prefaces the statement with "my intuition tells me", so perhaps he is much less categorical (pun intended) about the claim than you interpret it.

It is correct, in the best possible way.

Having least structure is a soft/aesthetical statement, and the explanation is right after it (a correct definition).

I wish all the math looked like this, first a soft/aesthetical statement, then right after the correct math.

Better thread on Mastodon [1]

[1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277

"Set-theoretic type theory" is working with the lattice of all subsets of possible values, where a "type" is one of these subsets. This lattice has plenty of structure, but sure individual subsets do not.

The category of sets is different from this lattice, since it allows arbitrary functions between sets for its morphisms rather than just inclusions.

"Set-theoretic types" have a meaningful notion of overlap. Usually types in other type system tend to be practically disjoint, like objects in a concrete category might be sets but the category itself doesn't give language to check whether the objects are disjoint sets.

Interesting definition of most structure

Reply on news.ycombinator.com