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?