> 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.