$f : ℕ 1 → ℕ 1$