 Type-shifting automorphism

For an integer-indexed typed model, a type-shifting automorphism is a bijection from each type to the next preserving equality, adjacent-type membership and the set predicates. On type zero define $xEy$ by $x\in j(y)$. Stratified formulas are translated by sending a variable of type $i$ to $j^i(x)$. Typed comprehension then gives the untyped comprehension of NFU. Such an automorphism is external; formulas containing it are not included in the typed comprehension scheme.