Impredicative

參考 https://github.com/AndrasKovacs/elaboration-zoo/tree/master/06-first-class-poly

In type theory

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} : (a : U_k) \to \ldots

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

In Elaboration algorithm

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