Universe polymorphism comment

Coq implements a rule called cumulativity (which is independent from the CoC) which extends the judgement of universes to Type@{i}: Type@{j} for i < j. This makes it so that higher universes as essentially “larger” than lower universes, as if the lower universes were literally included in the higher ones.

This is correct, but it's incomplete in that it doesn't capture the inference principle x : Type@{i} |- x : Type@{j} for i<j. For example, nat : Set and Set : Type@{u}, therefore nat : Type@{u} for any u. But nat is not of the form Type@{i}, so this doesn't follow from the rule above.

Start by locating the documentation passage containing the quoted explanation of cumulativity and universe levels. Read the surrounding discussion, then update the explanation so it also accounts for the stated inference principle; done means the example and the rule are both accurately described.