Universe variables

So far we've used A: Type* to declare a type variable A that works for any universe (universe polymorphic). In this situation Leans creates a universe variable, say u₁ and uses it instead.

We can introduce universe variables explicitly with statements like

universe u
-- or
universes u v

In the definition of Vec , if we were to use Type* in both places Lean would try to crate two independent universe variables (say, u₁, u₂).

This would be incorrect, as there are some constraints that universes variables most follow: If we create an inductive type I parameterized by a type A in universe u, the resulting type I can't live in a universe smaller than u (with one exception, Prop, to be discussed in the future).

Long story short, using a single universe variable u ensures that Vec inhabits the same universe that the parameter A, satisfying Lean's universe rules.