Note: I'm approaching this from a purely syntactic perspective. I'm sure that a deeper answer could be given from the semantic perspective. And apologies in advance for the poor formatting, I'm not at a computer right now.

In all type theories I'm aware of, a universe is a type that classifies types. You mention the idea of a type-term distinction. I'm interpreting this as the presence or absence of a judgment of the form A type, separate from x : A. This naturally leads to two styles of adding a universe to a type theory: universes ala Russel (Russel universes) and universes ala Tarski (Tarski universes).

A Russel universe is some type U, whose elements are other types. If we have some type ℕ, then we can derive a the judgment ℕ : U. The presence of a Russel universe allows us, if we wish, to completely eliminate any separate A type judgment, replacing it with A : U (assuming we have some type for U itself). This solution is conceptually straightforward and is used in languages like Coq and Agda.

A Tarski universe is also some type U, but instead of its elements being types, they are instead terms, which we call type codes. Basically, instead of being able to derive ℕ : U, we have some new term, which I will call 'ℕ, for which we can derive the judgment 'ℕ : U. We do this for each type former. Notably, 'ℕ is not a type. We cannot derive 'ℕ type or zero : 'ℕ. Instead, we introduce a special syntax which allows us to transform a type code into a type. This syntax is usually called El (short for element), and allows us to derive that El(a) type given that a : U. In order to make El useful, we introduce the "obvious" judgmental equalities: for instance that El('ℕ) = ℕ type. If instead we made these judgmental equalities into mere equivalences, where an explicit coercion is required to transform a code into a type, we would have what are called weak Tarski universes. For a language that actually implements weak Tarski universes (though they are essentially hidden by elaboration), check out cooltt: https://github.com/RedPRL/cooltt.

So to answer your questions with all this in mind:

1. Yes
2. A type is a universe when its elements classify other types in some meaningful way
3. I would say that this is wrong, but I do not have enough knowledge of semantics to back up why it must be
4. Tarski universes
5. Not necessarily, if we have a cumulative hierarchy of universes, we could have a rule classifying a type in any universe level
6. Universes exist globally in all type theories with them that I know of

Note: I'm approaching this from a purely syntactic perspective. I'm sure that a deeper answer could be given from the semantic perspective.

In all type theories I'm aware of, a universe is a type that classifies types. You mention the idea of a type-term distinction. I'm interpreting this as the presence or absence of a judgment of the form $A \ type$, separate from $x : A$. This naturally leads to two styles of adding a universe to a type theory: universes ala Russel (Russel universes) and universes ala Tarski (Tarski universes).

A Russel universe is some type $U$, whose elements are other types. If we have some type $ℕ$, then we can derive a the judgment $ℕ : U$. The presence of a Russel universe allows us, if we wish, to completely eliminate any separate $A \ type$ judgment, replacing it with $A : U$ (assuming we have some type for $U$ itself). This solution is conceptually straightforward and is used in languages like Coq and Agda.

A Tarski universe is also some type $U$, but instead of its elements being types, they are terms, which we call type codes. Basically, instead of being able to derive $ℕ : U$, we have some new term, which I will call $`ℕ$, for which we can derive the judgment $`ℕ : U$. We do this for each type former. Notably, $`ℕ$ is not a type. We cannot derive $`ℕ \ type$ or $zero : `ℕ$. Instead, we introduce a special syntax which allows us to transform a type code into a type. This syntax is usually called $El$ (short for element), and allows us to derive that $El(a) \ type$ given that $a : U$. In order to make $El$ useful, we introduce the "obvious" judgmental equalities: for instance that $El(`ℕ) = ℕ \ type$. If instead we made these judgmental equalities into mere equivalences, where an explicit coercion is required to transform a code into a type, we would have what are called weak Tarski universes. For a language that actually implements weak Tarski universes (though they are essentially hidden by elaboration), check out cooltt: https://github.com/RedPRL/cooltt.

So to answer your questions with all this in mind:

1. Yes
2. A type is a universe when its elements classify other types in some meaningful way
3. I would say that this is wrong, but I do not have enough knowledge of semantics to back up why it must be
4. Tarski universes
5. Not necessarily, if we have a cumulative hierarchy of universes, we could have a rule classifying a type in any universe level
6. Universes exist globally in all type theories with them that I know of