Is Morse-Kelley set theory with Class Choice bi-interpretable with itself after removing Extensionality for classes?

Question

Let $\sf MKCC$ stand for Morse-Kelley set theory with Class Choice. And let this theory be precisely $\sf MK$ with a binary primitive symbol $\prec$ added to its language, and the following axioms ensuring that $\prec$ is a well-ordering on classes.

$\textbf {Transitive: }X \prec Y \land Y \prec Z \to X \prec Z \\ \textbf{Co-Connected: } X \not \approx Y \iff [X \prec Y \lor Y \prec X] \\ \textbf {Well-Founded: } \phi(X) \to \exists Y: \phi(Y) \land \forall Z [\phi(Z) \to Z \not \prec Y], \text { for every formula } \phi$

Where: $X \approx Y \iff \forall z \, (z \in X \leftrightarrow z \in Y)$.

Let $\sf MKCC'$ be the theory $\sf MKCC$ with axiom of extensionality replaced by an axiom of extensionality for sets only.

Is $\sf MKCC'$ bi-interpretable with $\sf MKCC$?

Answer 1

No, because the latter theories has parametrically definable automorphisms that swap two equivalent classes, but the former theory is definably rigid (no need for class choice). If the theories were bi-interpretable, then we could fix a copy of the model with two equivalent classes (having the same elements), and inside this model we could define a copy of MK, and inside that define a copy of the original model, but because the automorphism would have to fix the definable interpretation but swap the classes, it would ruin the bi-interpretability feature.