Call a type of structure **rigid** if any automorphism of such a structure is an identity.  (This is a bit different from some other uses of the word, but hopefully I'll be forgiven.)  For example, well-orderings are rigid.  It follows that assuming the axiom of choice, there is a rigid type of structure (namely, a well-ordering) such that *any* set can be equipped with that type of structure (in a non-unique way, of course).

Now the axiom of choice isn't necessary for that conclusion.  Extensional well-founded relations are also rigid, and the axiom of foundation implies that any set injects into an extensional well-founded relation (its transitive closure).  Aczel's axiom of anti-foundation also suffices, since [strongly extensional relations](http://ncatlab.org/nlab/show/extensional+relation) are also rigid, and anti-foundation implies that any set injects into such a relation.  But with neither foundation nor anti-foundation, the membership relation $\in$ needn't be rigid.  For instance, the set {a,b}, where a={a} and b={b} are unequal ill-founded sets with the same membership tree, has a nonidentity $\in$-automorphism which swaps a and b.

Now my question: If we don't assume choice or any sort of foundation, does there still exist a *rigid* type of structure with the property that *any* set can be equipped with that type of structure?

**Edit:** Of course, as Steven points out in the comments, I haven't said exactly what I mean by "type of structure."  I'm using the word "structure" in the Bourbaki-sense, not in the sense of [stuff, structure, property](http://ncatlab.org/nlab/show/stuff,+structure,+property).  Here's one way to make this question precise: does there exist a theory in higher-order logic which is rigid, in the sense that any automorphism of one of its models is the identity, and which admits a definable functor to Set which is essentially surjective?