Yes, I misread your description of a set as formalized by a sequence
of '0's, '1's, and '2's as your encoding upon which you based your
equality. As it is based on this other equality, there /is/ a
bijection such that AA = A, AB = BA, etc.

A recursive version of your encoding f : HF -> N is described by:

f({}) = 0
f(A) = sum{x in A} 2^f(x).

(I write "sum", but it would be more appropriate to use bitwise or).

f is well-defined for HF sets; since HF sets are well-founded (no
infinite descending chains of membership). This is what I assume your
rule (3) is trying to say.

Note that if x in A, then f(x) < f(A).

If we write "v" for bitwise or, "&" for bitwise and, "!=" for not
equals, and consider 2^x as a single bit shift, then we can prove that

x in A iff ((2^f(x)) & f(A) = (2^f(x)))

so f is an injection.

The inverse encoding g : N -> HF is defined recursively as:

g(0) = {}
g(n) = { g(m) : 2^m & n = 2^m}

g is well defined, since if 2^m & n != 0, then m < n.
Again, g is an injection. And

g(f({})) = {}
g(f(A)) = {g(f(x)) : 2^f(x) & f(A) = 2^f(x)}
        = {g(f(x)) : x in A}

By induction staring with g(0), and noting that x in A -> f(x) < f(A),
we can then deduce that g(f(A)) = A; so since g and f are injections,
g is the inverse of f, and f is a bijection.

As regards your production rules, the naturals do provide a model
using f:

Define:
"A is a set" iff A = 0 or A = 2^n for some n.
"A are sets" iff not (A is a set)
"{}" = 0.

"{} is a set."
0 is a set.

"If A is a set or are sets, then {A} is a set."
Define {A} = 2^A; then {A} is a set.

"If A is a set and B is a set then AB are sets"
In this case, we define AB = 2^A v 2^B; so AB are sets.

"If A is a set and B are sets then AB are sets"
In this case, we define AB = 2^A v B; again AB are sets.

"There are no other ways of forming sets."
This is your vaguest axiom; it would be better to say that every set/
sets /can/ be formed in this way through a finite sequence of
applications of rules 0, 1, and 2 (or state it as the contrapositive).
We can take it as saying that every natural A is either 0, or is the
sum (bitwise or) of one or more powers of 2, each of those powers
being less than A; and we can satisfy the requirement via induction.

Because of the function g, the HF sets are also a model; "A is a set"
means |A| = 0 or 1, "A are sets" means |A| > 1, {A} is defined as
usual, and AB = {A} union {B} or {A} union B depending on whether B is
a set or are sets.