8.3 Ambiguity
Let \( L \) be an \( \mathbb N \)-language. A type raising morphism is a map of languages \( L \xrightarrow {\operatorname {\mathsf{succ}}} L \), where \( \operatorname {\mathsf{succ}} : \mathbb N \to \mathbb N \) is the successor function.
The remainder of this chapter is left unfinished until we finish the main part of the project.