A universe is impredicative if function types whose codomains are in the universe are always in the universe, regardless of their domain types.

如果 $\text{foo} : U_k$ 可以通過檢查，這個 Universe $U_k$ 就是 impredicative 的，有 impredicative universe 存在的類型理論就叫做有 impredicativity。像 Rocq 或是 Lean 都有特殊的 Prop universe 有這樣的特性。

An elaboration algorithm is impredicative if it is able to solve metavariables to implicit function types.