It's not an isomorphism though, it misses the always true map. This means that many predicates on nat do not terminate on nat -> bool.