Types are defined by the structure of values (two differently-named types which are arrays of 5 ints are the same type). See NominativeAndStructuralTyping.
I do not think that upcasting constitutes a change of type, but downcasting certainly does.
Huh? This would require some strange rules for type (in)equivalence, or it could be argued that with B-(up)->A-(down)->B the two B-s end up with different type. (The type of A is equal to the first B but different from the second B.)
TypeInference is a separate issue; like optimization I'd consider it a compiler feature rather than a language feature. Type inference is definitely a language issue, since it dictates where type information must be written or can be elided in the source text.
There is TypeInference as an optional compiler feature, but more often TypeInference is a feature of a language; pure functional languages like Haskell cannot be implemented without it.
Huh? There are dynamically-typed functional languages, such as LispLanguage. Plus, I'm sure one could write a functional language with ManifestTyping, though I'm not sure one would want to. LispLanguage is not a pure functional language.
Um, there are typeless pure functional languages, such as the pure lambda-calculus, so the claim about the necessity of TypeInference is obviously false.
There are three axes here: static-dynamic, strong-weak and nominative-structural. You can choose to look at each as boolean (either types can be changed or they can't) or a continuum. When considering whether a language has any of these attributes, it may be most productive to consider not just what is possible in a language, but what is encouraged.
Other type terms that need simple definitions: