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.
> 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.
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.
This is all false. What you describe is a violation of the Archimedean principle. "Numbers" are a wider concept than the Archimedean principle.
So let’s play that old 21s drinking game, but infinitely instead of 1 to 21, and rename 1 to 1, 2 to 4, 3 to 9 and so on, up to x for any x. Same set, different lingo.
That you can’t map back 5 is irrelevant although kind of leaves a bad taste.
You need neither though. For example:
y = x ^ 2 when even, (x+1) ^ 2 otherwise
It's a bijection. (And therefore obviously also a surjection.) "One-to-one correspondence" is a correct, but incomplete, description.
Unless you consider the domain of f the "renamed" range, in which case yes tautologically it is bijective.
You seem to be talking about the function f: N -> N, which isn't surjective, but I don't see the relevance. Any surjective function can be made non-surjective by considering a larger range.
It's worse than just irrelevant. The claim is that we have two sets, ℕ and S, that are the same size. The argument that they are the same size is the observation that we've demonstrated a bijection between them.
No one ever mentioned a function from ℕ to ℕ, because that would tell you nothing about S. It would be like saying "in order to show that 5 is odd, observe that 2 and 2 are both even". The idea is gibberish.