3
$\begingroup$

Let's say we work in a dependent type theory with W-types and we want to have a type for binary natural numbers. We don't want to add quotient types or higher inductive types to the system.

How to represent the idea that leading zeroes don't change the natural number? Do we necessarily enter setoid territory at this point?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

Use an auxiliary type of positive natural numbers.

data positive : Set where
  one : positive
  s0  : positive → positive -- multiply by 2
  s1  : positive → positive -- multiply by 2 and add 1

data N : Set where
  zero : N
  pos : positive → N

Supplemental: Another option, which I found on my whiteboard today (probably put there by Egbert Rijke months ago) is this:

-- Dyadic natural numbers without redundancy
data N : Set where
  zero : N      -- 0
  suc0 : N → N  -- suc1 n = 2 * n + 2
  suc1 : N → N  -- suc1 n = 2 * n + 1

I think you'll probably prefer this one.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ You want to omit “one” from the whiteboard definition, as it already has a different representation. These are the dyadic numerals, by the way, rather than binary. $\endgroup$
    – Emil Jeřábek
    Mar 17, 2021 at 16:58
  • 1
    $\begingroup$ Better link: en.wikipedia.org/wiki/Bijective_numeration. $\endgroup$
    – Emil Jeřábek
    Mar 17, 2021 at 17:01
  • $\begingroup$ Thanks for the links and the useful information. I fixed the definition. $\endgroup$
    – Andrej Bauer
    Mar 17, 2021 at 18:28

Your Answer

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