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