Abstracting over large types in type theory

Question

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.

Answer 1

What you suggest is possible for certain kinds of type theories. For example, the $\lambda$-calulus $F_\omega$ (see Figure 2 of this paper) supports universal quantification over all types, and even higher-rank types. Note that $F_\omega$ is not dependently typed.

A universe of types $U$ which is closed under products indexed by $U$ is called an impredicative universe. What you are suggesting corresponds to working in an impredicative universe. In Coq Prop is such a universe, and one can also enable an option that turns Set into an impredicative universe.

One needs to be careful about combining impredicative universes with other features. Please consult Coq.Logic.Hurkens for references and formalization of some results in this direction. For example, one cannot have an impredicative universe with an impredicative universe inside it.

We can also bring in types as parameters in a limited way which does not allow us to form $\Pi(A \; \mathsf{type}) . B(A)$ and $\Sigma(A \; \mathsf{type}) . B(A)$. One such approach is (first-order) parametric polymorphism in which all type parameters must appear at the front, and cannot be quantified over (in the style of parametric polymorphism in OCaml, ML, and Haskell). In other words, we may use type variables schematically. In a sense, Coq does this, except that it introduces universe polymorphism, i.e., universe indices can be used schematically, as that is sufficient to then express type parameters: instead of saying "for all types $A$ ..." we say "for all universe indices $i$, and all $A : \mathsf{Type}_i$, ...".