4 ms·

Your failure to do the actual renaming doesn't make the renaming a failure. No one has claimed that the set of squares is extensionally equal to the naturals. T

Your failure to do the actual renaming doesn't make the renaming a failure. No one has claimed that the set of squares is extensionally equal to the naturals. The existence of a bijection has nothing to do with extensional equality of the given sets. It's not even a particularly strong equivalence among those in everyday use. I guess the category theorists have a cute name for this (morphism? Who knows...), but it is to set cardinality as homomorphism are to groups. But in fact even if the claim had been about extensional equality, HoTT shows how this can be carried out correctly: the equivalence between two types (which is supposed to be actual Leibniz equality, not merely equinumerosity as in the example) must be used, as if a function, to transport actual terms between the two types. Using this mechanism, the subtype of square naturals is in fact extensionally equal to the naturals. For example, the term `f 4` where `f` is the transport along `squares = N` is in fact the sum of the multiplicative identity with itself. This is what I meant by actually doing the renaming.

cubefox 3y ago
He said "just" a renaming, which suggests just the names change while the meaning stays the same, which isn't the case. Maybe he meant it in some different "HoTT" sense, but he clearly said > Given that a one-to-one correspondence is just a renaming, and renaming things doesn't change how many there are, this seems sound. which would only be the case for renaming salva veritate -- or by begging the question in favor of one-to-one correspondence being sufficient for something being the "same size" and against proper subsethood being sufficient for something being not the same size. But that's exactly the question when arguing for or against Hume's Principle, not something which can be assumed.
- thaumasiotes 3y ago
  > He said "just" a renaming, which suggests just the names change while the meaning stays the same, which isn't the case. Huh? That's exactly what's happening. If you rename 1, 2, and 3 to one, two, and three, the names have changed and the meanings haven't. As you note, this is what "renaming" means. It used to be true that 1 + 2 = 3, but now that's gibberish and one + two = three instead. Nothing about that changes if you instead rename 1, 2, and 3 to 88, 89, and 90. It will still be true that 88 + 88 = 89. You don't get to reinterpret what the name means after you assign it.
  - cubefox 3y ago
    Well, then the squares are still a proper subset of the natural numbers, while still being in a one-to-one correspondence, so Galileo's Paradox remains. Then renaming didn't change anything.

cubefox 3y ago

He said "just" a renaming, which suggests just the names change while the meaning stays the same, which isn't the case. Maybe he meant it in some different "HoTT" sense, but he clearly said > Given that a one-to-one correspondence is just a renaming, and renaming things doesn't change how many there are, this seems sound. which would only be the case for renaming salva veritate -- or by begging the question in favor of one-to-one correspondence being sufficient for something being the "same size" and against proper subsethood being sufficient for something being not the same size. But that's exactly the question when arguing for or against Hume's Principle, not something which can be assumed.

thaumasiotes 3y ago
> He said "just" a renaming, which suggests just the names change while the meaning stays the same, which isn't the case. Huh? That's exactly what's happening. If you rename 1, 2, and 3 to one, two, and three, the names have changed and the meanings haven't. As you note, this is what "renaming" means. It used to be true that 1 + 2 = 3, but now that's gibberish and one + two = three instead. Nothing about that changes if you instead rename 1, 2, and 3 to 88, 89, and 90. It will still be true that 88 + 88 = 89. You don't get to reinterpret what the name means after you assign it.
- cubefox 3y ago
  Well, then the squares are still a proper subset of the natural numbers, while still being in a one-to-one correspondence, so Galileo's Paradox remains. Then renaming didn't change anything.