> Type annotation helps partially here since you can statically check the types notated post facto but this is not the type system.hatever a static type checker enforces is exactly a type system (and the only thing that is), in the standard CS sense.

The fact that the type checker isn't integrated with the compiler/interpreter is a different design choice from other systems, but it doesn't change what it is.

Effectively, mypy (and this was explictly what mypy was originally envisioned as, as is still reflected in its domain name) and other typecheckers for Python create separate statically typed languages with the same relation to Python as TypeScript has to JavaScript, except that source code in those languages is also valid Python source code with identical runtime behavior. That is, each typechecker creates a new language that is a statically typed strict subset of Python, with its own type system (most of which is common across the whole set of languages, but there are slight variations as each are ahead of the common baseline in different ways.)

> The type system in a language is a contract by the compiler/interpreter to enforce type safety

No, it's enforced by the typechecker. Now, in most languages implementations that have a type system, that's part of the compiler, or more rarely interpreter, but there is no inherent reason it needs to be.

> This is why I'm trying to draw the distinction between the type system vs the type annotation system.

Yes, you've invented artificial nonstandard terminology here that is clearly not the terminology that was being in the post you argued against, in order to make a really extended argument that vigorously exercises the fallacy of equivocation and badly misses the point of the post it sought to dispute.

To the extent there is a legitimate point here it boils down to “Strictly speaking, Python remains untyped, and what is advancing are the type systems of a family of statically typed languages built around Python, that are strict subsets of Python, that leverage feature built in to Python specifically to enable such languages, and which are developed in close collaboration with Python, in some cases sharing core team members.”