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.