Hacker News new | ask | show | jobs
by AlexSW 1015 days ago
Why should one be bothered by it?
2 comments

It makes a simple thing (pair) complicated.

This may be true for Category Theory as well (Product of two objects):

https://en.wikipedia.org/wiki/Product_(category_theory)

But Category Theory captures the essence of Products/Pairs, so I am more inclined to accept it.

> It makes a simple thing (pair) complicated.

Well, yeah, but {x, y} is also a pair. How is (x, y) different? It's ordered, you say? All right, an ordering is a relation that's antisymmetric and so on, but in this case let's say we have a function that maps x to 0 and y to 1… But what is a function? Okay, a function is a type of relation, so let's define a relation first: a set of ordered pairs… oops.

The real problem with defining (x, y) = {{x}, {x, y}} is that elements of a set must also be elements of some universal set 𝓤, {x, y} ⊂ 𝓤, but as we know, there is infamously not such a thing as a "set of all things". Sets have to be typed. But in a pair, x and y can be of entirely different kinds of entities.

Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).
It seems to be ignoring β-reduction for one.

But an ordered set is fundamentally different than an unordered set as well!