Various mechanisms are available for managing universe levels in proof assistants based on type theory. The Agda proof assistant implements a strong form of universe polymorphism in which universe levels are internalised as a type, making levels first-class objects and permitting higher-rank quantification via ordinary Π-types. We prove normalisation and decidability of equality and type-checking for a type theory with first-class universe levels inspired by Agda. We also show that level primitives can safely be erased in extracted programs. Our development is formalised in Agda itself and builds upon previous work which uses logical relations on extrinsically typed syntax.