[001X] -- Synthetic topos theory

- $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})$ .