In dependent type theory usually the typing context lets you abstract over arbitrary elements of some (dependent) types. Now if one wants to abstract over an arbitrary (but not quite) type, they can use a universe construction. To stay consistent we can't allow the universe to contain itself. So one can only abstract over small types that are contained in some universe.
E.g. here is a typing signature in some hypothetical dependent type theory:
(A : 𝕌) (B : 𝕌) (f : A → B) ⊦ map : List A → List B
My question is, can't we allow to abstract over a typing judgement (A type)
instead of abstracting over a small type (A : 𝕌)
(A type) (B type) (f : A → B) ⊦ map : List A → List B
If we could do that consistently, it would be so much easier than current universe approaches involving universe levels, universe polymorphism, etc.
Π (A type). B
andΣ (A type). B
? If not, then what you are suggesting is that we allow type parameters a la first-order parametric polymorphism, which sounds harmless enough. If you allow products that range over all types, you're in trouble. $\endgroup$