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.