Overall I like the PEP and examples.
One more thing you might consider writing an example for: cython. It should be feasible for a future cython to understand typing.Annotated based annotations that contain the cython type so that cython code can be both pep484 type checked _and_ cython compiled down to faster code due to the cython c types specified via annotation.
Perhaps reach out to the Cython project and see what they think?
I don't anyone to love the potential extra verbosity that comes when you have annotations for multiple purposes at once, but you do already cover that in the PEP in what seems like a reasonable manner.