Pair a b = Set (Either a (Set (Either a b)))
  mkpair a b :: a -> b -> Pair a b
  mkpair x y = {left a, right {left a, right b}}

These "is-a" relations simply give one way of implementing maps and
pairs in a seldom-used programming language called ZF, and they are
not very helpful in conveying and understanding what maps and pairs
are about.  If maps and pairs are thought of as abstract data types,
an abstract specification is called for, and chances are it is more
enlightening, e.g.,

  (x,y)=(a,b) iff x=a and y=b

is infinitely more readable, useful, and to the point than any
set-theoretic encoding.

Furthermore, sets are not always more primitive, and maps are not
always derived from sets in implementations.  In PalmOS, maps or
relations are primitive, and if you want a set, you ought to derive
one from relations.

A specification for maps, whether in the form of a bunch of axioms
concerning lookups, or as an equation with a certain set, must be
judged on its merit as a specification (is it understandable, does it
help reasoning about programs using it), not on how faithfully it
copies from the foundations of mathematics.  No one specifies the
integer data type as equivalence classes of pairs of natural numbers
under the relation (m,n)~(j,k) iff m+k=n+j.  (On the other hand, when
specifying stacks, I still find it easier to encourage the audience to
imagine consing and tailing a cons list.)

The reason explained below may or may not be a good reason to say maps
are special sets; I don't know, because I don't understand it: