# Defining binary natural numbers without quotient types

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?

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.

• 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. Mar 17, 2021 at 16:58
• Better link: en.wikipedia.org/wiki/Bijective_numeration. Mar 17, 2021 at 17:01
• Thanks for the links and the useful information. I fixed the definition. Mar 17, 2021 at 18:28