Synthetic topos theory

[001U] Universe levels

We fix a universe hierarchy. There can be a lot of choices of universe hierarchy design. The following rules are a minimal requirement.

[001V] Rule

\(\mathord {\textnormal {\textsf {Level}}}\) is a judgment form.

[001W] Rule

Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\). Then \(i_{1}\le i_{2}\) is a propositional judgment form.

[001X] Rule

  • -\(0:\mathord {\textnormal {\textsf {Level}}}\).
  • -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {succ}}}(i):\mathord {\textnormal {\textsf {Level}}}\).
  • -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(i\le i\).
  • -Let \(i_{1},i_{2},i_{3}:\mathord {\textnormal {\textsf {Level}}}\) and suppose that \(i_{1}\le i_{2}\) and that \(i_{2}\le i_{3}\). Then \(i_{1}\le i_{3}\).
  • -Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\) and suppose that \(i_{1}\le i_{2}\) and that \(i_{2}\le i_{1}\). Then \(i_{1}\equiv i_{2}\).
  • -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(0\le i\).
  • -Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(i\le \mathord {\textnormal {\textsf {succ}}}(i)\).
  • -Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\) and suppose that \(i_{1}\le i_{2}\). Then \(\mathord {\textnormal {\textsf {succ}}}(i_{1})\le \mathord {\textnormal {\textsf {succ}}}(i_{2})\).

[002F] Definition

We define \(1:\mathord {\textnormal {\textsf {Level}}}\) to be \(\mathord {\textnormal {\textsf {succ}}}(0)\).