  We provide a "shared axiomatization" of natural numbers and hereditarily
finite sets built around a polymorphic abstraction of bijective base-2
arithmetics.
  The "axiomatization" is described as a progressive refinement of Haskell type
classes with examples of instances converging to an efficient implementation in
terms of arbitrary length integers and bit operations. As an instance, we
derive algorithms to perform arithmetic operations efficiently directly with
hereditarily finite sets.
  The self-contained source code of the paper is available at
http://logic.cse.unt.edu/tarau/research/2010/unified.hs .
