Does the "Every epimorphism splits" form of the axiom of choice imply LEM in constructive type theory?

Usually the axiom of choice is formulated as follows in dependent type theory:

$$\prod_{a : A} \sum_{b : B} A(a,b) \to \sum_{f:A
\to B} \prod_{a:A} A(a,f(a))$$

And according to Wikipedia, this does not imply the law of the excluded middle, because Diaconescu's theorem depends on the axiom of separation, which constructive type theories generally do not have an equivalent to.

However, how do other forms of the axiom of choice fair in contstructive type theory? Specifically, concerning the following:

$$ \prod_{f:A \to B} ((\prod_{C : Type} \prod_{g, h : B \to C} (g \circ f = h \circ f \implies g = h)) \implies \sum_{f^{-1} : B \to A} f \circ f^{-1} = Id_B)$$

which intuitively says that "all epimorphisms split" when viewing the type theory as a category. Is this provable in (say) basic Martin Lof Type Theory? Does it imply the law of excluded middle?

Answer

In constructive type theory, the extensional form of the axiom of choice is in fact equivalent to the statement "all epimorphisms split". And hence, by the usual argument, implies LEM. See theorem 1 of Martin-Löf's paper on the subject.