New Foundations is consistent

8.3 Ambiguity

Definition 8.13
#

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.