Collects and maintains the set of types relevant to a proof.

The type universe determines which polymorphic constants ($=_\tau$, $\Pi_\tau$, $\Sigma_\tau$) are available as heads in general bindings for primitive substitution. It contains every type and sub-type occurring in the problem signature as well as every type introduced at runtime by skolemization or renaming.

A type $\alpha_1\to\cdots\to\alpha_n\to\gamma$ decomposes into:

• the type itself,
• every proper suffix $\alpha_k\to\cdots\to\alpha_n\to\gamma$,
• the base type $\gamma$, and
• recursively, the sub-types of each $\alpha_i$.