4 ms·

> 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, sin

by pizza 3y ago

> 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/1674357272498110467 https://twitter.com/BartoszMilewski/status/16743572724981104...

climatologist 3y ago
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.
- klysm 3y ago
  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.
- js8 3y ago
  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.
- bmacho 3y ago
  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.
louthy 3y ago
Better thread on Mastodon [1] [1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277 https://mathstodon.xyz/@johncarlosbaez/110631013611448277
klysm 3y ago
Interesting definition of most structure
kmill 3y ago
"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.

by pizza 3y ago

climatologist 3y ago

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.

klysm 3y ago
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.
js8 3y ago
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.
bmacho 3y ago
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.

louthy 3y ago

Better thread on Mastodon [1] [1] https://mathstodon.xyz/@johncarlosbaez/110631013611448277 https://mathstodon.xyz/@johncarlosbaez/110631013611448277

klysm 3y ago

Interesting definition of most structure

kmill 3y ago

"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.