I feel like the explanation is overcomplicated. Types are properties of values, not variables. Mutability is a property of variable, not of a value.
So it's kind of a categorical error. (I want to joke here that all categorical errors are just type errors in category theory.) When we speak of "type of a variable", we mean this variable can only be assigned (bound to) values of certain type. This has nothing to do with whether it can be reassigned (i.e. mutability).
So you don't even need the notion of subtyping to explain this.
Also, one could probably define variable as a monad over its type.
So it's kind of a categorical error. (I want to joke here that all categorical errors are just type errors in category theory.) When we speak of "type of a variable", we mean this variable can only be assigned (bound to) values of certain type. This has nothing to do with whether it can be reassigned (i.e. mutability).
So you don't even need the notion of subtyping to explain this.
Also, one could probably define variable as a monad over its type.