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 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. 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?