1
$\begingroup$

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: enter image description here

$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$
    – Trebor
    Apr 27, 2023 at 1:20
  • $\begingroup$ You can still express this function using the sliding window trick, but it is no longer of the eliminator-form. $\endgroup$
    – Trebor
    Apr 27, 2023 at 1:22
  • $\begingroup$ 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. $\endgroup$
    – Russoul
    Apr 27, 2023 at 1:32
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 27, 2023 at 8:50
  • 1
    $\begingroup$ It is considered bad form to post pictures of code. You're behaving like my children. $\endgroup$ Apr 27, 2023 at 20:44

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
2
  • 6
    $\begingroup$ 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. $\endgroup$ Apr 27, 2023 at 13:01
  • 1
    $\begingroup$ Imagine if they were unprovably different! $\endgroup$ Apr 27, 2023 at 20:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.