@lisyarus Turing completeness is the empirically unique reasonable notion of computability for functions Nat -> Nat, but for (Nat -> Nat) -> Nat (aka type-2 computability) there are multiple reasonable notions of computation that are not equivalent, so there is no such thing as “Turing completeness” there