ct.category theory - A rigid type of structure that can be put on every set?

This doesn't completely answer the question, but I think it's relevant.

Theorem: Let T and W be theories in higher-order logic (by which I mean the internal type theory associated to elementary topoi), where W has a specified underlying object X (i.e. we regard a model of W as an object X equipped with some additional stuff). Then it is not the case that both (1) T proves that W is rigid (as structure on X) and (2) in any topos satisfying T, every object can be equipped with W-structure.

Proof: Suppose that both the given conditions hold. Let C[T,X] be the free topos on the theory T and an additional object X, and let C[T,W] be the free topos on T and W. (Recall that for any theory S and any topos E, the category Log(C[S],E) of logical functors and natural isomorphisms from C[S] to E is equivalent to the category of models of S and their isomorphisms in E.) Now the generic model of W in C[T,W] has an underlying object, giving a logical functor C[T,X]→C[T,W]. And C[T,X] satisfies T, so by assumption, its generic object X can be equipped with W-structure; thus we also have a logical functor C[T,W]→C[T,X], and the composite C[T,X]→C[T,W]→C[T,X] is isomorphic to the identity. In other words, C[T,X] is a pseudo-retract of C[T,W]. Now let E be any other topos satisfying T and Y any object of E admitting a nonidentity automorphism (such as Y=1+1); then we have a logical functor C[T,X]→E sending X to Y, which in turn has a nonidentity automorphism. But because C[T,X]→C[T,W]→C[T,X] is the identity, this functor C[T,X]→E must factor through C[T,W], and since T proves that W is rigid, any automorphism of this functor must be the identity, a contradiction. ∎

This means that if you want a rigid type of structure that can be put on every set, you need to use more about sets than the fact that they form an elementary topos, or even a Boolean topos with a NNO, or any additional property of Set that can be expressed as a theory T in HOL. Note that AC, although it can be phrased as a "categorical" property not referring directly to ∈ (every surjection splits), cannot be expressed as a theory in HOL since it involves a quantification over all sets. Likewise for the "topos-theoretic axiom of foundation" that every set injects into some well-founded extensional relation. So the question is, what can we do with the remaining non-HOL axioms of ZF, i.e. basically replacement and (its consequence) unbounded separation.