[ex3xu]

You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way.

> The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory.

I'm getting confused because Martin-Lof writes at the end of this paper:

> I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice...

Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.

[tines]

I'm confused then because the paper linked in the OP states:

> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]

[pfortuny]

It is choice in constructible mathematics: something “totally different” from “zf” choice. Existence means “can construct”, essentially. There are “less” things in constructible mathematics than in zf. This is a rough explanation.