Good question. I don't think anyone has ever asked this before... Given the variants you propose, I'd say that the 3-character ones would be more effort to type without real benefits, and `=>` would at the time (and perhaps still :-) be seen as too close to `>=`.
Could it be that there were already other languages using `->` for return types? I do know that we needed something there -- from the start I was a fan of `x: int` because it's the same as Pascal (the language I used most intensely in college), and if it had been syntactically possible I would have used 'def f(): int' for the return type as well, but the LL(1) parser in use in 1999-2000 would interpret that as a very short function body.
It's also possible that it comes from the `->` operator in C, which would be the only "ASCII art arrow" that I was familiar with at the time.
Note that a slide deck I presented in 2000 on the topic still exists:
https://gvanrossum.github.io/static-typing/ This shows something pretty close to the modern notation for function and variable annotations, but with a `decl` keyword thrown in.