Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator

In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ℕ -> A is equal to the "eliminator" arrow for some pair of arrows init : 𝟙 → A, step : A → A. Is it true in some of the standard dependent Type Theories, say, in extensional MLTT or OTT?

Edit: as pointed out by Trebor, in the original formulation there are functions that can't be represented via the eliminator. But with an enhanced eliminator Trebor's example works:

• Consider the function $f(0)=f(1)=1$, $f(n)=2$ otherwise. This cannot be written in that form because you can't have step 1 = 1 and step 1 = 2 at the same time.
– Trebor
Apr 27, 2023 at 1:20
• You can still express this function using the sliding window trick, but it is no longer of the eliminator-form.
– Trebor
Apr 27, 2023 at 1:22
• That's not true. Assuming the following syntax: ⟨init, step⟩ : ℕ → A We have: ⟨1, ⟨1, const 2⟩⟩ 0 = 1 ⟨1, ⟨1, const 2⟩⟩ 1 = ⟨1, const 2⟩ 0 = 1 ⟨1, ⟨1, const 2⟩⟩ 2 = ⟨1, const 2⟩ 1 = 2 That is, step itself can be recursive. Apr 27, 2023 at 1:32
• Note that if you are given an eliminator elim which takes in only the weaker step : A → A, you can implement the stronger one by using elim at type A × ℕ and arrows built from the universal property of ℕ and the product. Apr 27, 2023 at 8:50
• It is considered bad form to post pictures of code. You're behaving like my children. Apr 27, 2023 at 20:44

With function extensionality this is trivially true, because f = elim (f 0) (\n _ -> f (suc n)). Without function extensionality I suspect it is not true, but constructing a countermodel would be hard because there is no recursion, just a single case split.
• The parametric exceptional model gives you a simple counter model of MLTT to this. In this model, constant functions fun (_ : nat) => t are provably different from their inductive η-expansion fun (n : nat) => match n with 0 => t | S _ => t end. Apr 27, 2023 at 13:01