宇宙

宇宙の列 $\mathcal{U}_0,\mathcal{U}_1,\ldots$ を置き、$\mathcal{U}_i:\mathcal{U}_{i+1}$ とする。各 $\mathcal{U}_i$ は $\mathbb{N}$、空の型 $\mathbb{0}$、1 元型 $\mathbb{1}$（元 $\star$）を含み、Π・Σ・Id で閉じている。$A:\mathcal{U}_i$ ならば $A$ は型であり、$A:\mathcal{U}_{i+1}$ でもある（累積性）。