Dependently types languages provide "pi types", that allow types to depend on the value of an input. My question is, what is the type of the pi type?
The type of a type is a universe. Usually, universes get stratified into levels like Type 0, Type 1, Type 2..., where the type of Type n is Type (n+1). The reason for this is that if we just had one level Type, the type of Type would have to be Type, which often leads to paradoxes.
So what is the type of forall a: A, P a (a pi type using Coq syntax)? If we assume that A: Type m and P: A -> Type n, we have forall a: A, P a: Type max(m, n). If we have cumulative universes (as Coq does), so that m≤n and A: Type m implies A: Type n, then really the type of forall a: A, P a is any universe that's larger than both m and n.
EDIT: In response to your comment, -> takes as arguments A: Type m and P: A -> Type n and returns forall a: A, P a, whose type is Type max(m, n), so the type of the pi constructor is forall (A: Type m) (P: A -> Type n), Type max(m, n), or, in Agda syntax, (A: Set m) (P: A -> Set n) -> Set max(m, n).