Universe Levels

In type theory, a universe level is an index for the (large) universe famies for example $\mathrm{Set}$, $\mathrm{Prop}$ and $\mathrm{Type}$ that acts as a (truncated) ordinal parameter for the universe.

Algebra

• $\ell 0:\mathrm{Level}$
• ${\_}^{+}:\mathrm{Level}\to \mathrm{Level}$
• $\bigsqcup :\mathrm{Level}\to \mathrm{Level}\to \mathrm{Level}$

Such that

• $(\mathrm{Level},\bigsqcup ,\ell 0)$ is an Abelian monoid.
• $\bigsqcup$ is idempotent
• $a\bigsqcup a^{+}=a^{+}$
• $(a\bigsqcup b{)}^{+}=a^{+}\bigsqcup b^{+}$