Defining binary natural numbers without quotient types
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.