$\sf MKCWO$ is the theory obtained by adding a new primitive binary relation $\prec$ to the signature of $\sf MK$ and axiomatize that $\prec$ is a well order on classes, that is:

 - $\textbf{Transitive:} X \prec Y \prec  Z  \to X  \prec Z $
 - $ \textbf{ Connected:}   X \neq Y \leftrightarrow [X \prec Y \lor Y \prec X]$
 - $\begin{align} \textbf{Well-Founded:}& \text { for each formula } \phi: \\ & \phi(X) \to \exists M: \phi(M) \land \forall Y \, (\phi(Y) \to \neg Y  \prec M) \end{align} $



What is the choice principle that needs to be added to $\sf MK$ in order to get an equivalent theory?

I was thinking of something along those lines:

To the language of $\sf MK$ add a monadic symbol $\varepsilon$ that takes a formula as an argument, such that for any formula $\phi$ having one free variable [whether set or class variable], the string $\varepsilon\phi$ is a term of the language. Then axiomatize:

 - $[\phi \leftrightarrow \psi] \to \varepsilon\phi = \varepsilon\psi$
 - $(\exists X\phi) \to\exists Y: Y=\varepsilon\phi$
 - $\phi(\varepsilon\phi)$

However, it's not clear to me how the second formulation can interpret the first one?

> Are these formulations equivalent?


> If not, can we express a choice principle whose addition to $\sf MK$ would be equivalent to $\sf MKCWO$?

**Note:** to avoid confusion in comments, the notation $\varepsilon$ replaced the older notation $c$. Also $\sf CWO$ replaced the older notation $\sf WO$.