Progress towards a computational interpretation of the univalence axiom?

Cubical type theory is a variant of type theory which has all the usual (and some unusal) computational properties, and the Univalence Axiom is a theorem of cubical type theory. As was already pointed out in the comments, there are implementations of cubical type theory that one can play with (even for 90 hours).

The Arend programming language provides an alternative approach. It does not actually provide a computational interpretation. Instead, it provides a function converting isomorphism into a path, and it built-in a computation rule that transportation along a path constructed from univalence will reduce to the application to the function in the isomorphism. In other words, it's type theory with the following primitives (simplified for reading ease -- the actual definitions are slightly more general):

• Isomorphism-to-path: iso : (Iso A B) -> A = B
• Transport: coe : A = B -> A -> B
• Computation rule coe (iso f) ==> f

If you look at the library, you'll see that even with these simple rules we can do a lot of HoTT already (from a type theoretical perspective, imagine a constructive version of MLTT with various extensionalities -- the community has done a lot with MLTT, and we can do everything there in Arend as well. Also, it has higher inductive types, so we can have some HoTT things there).

This style is similar to the HoTT-Agda library, but unlike the library, Arend doesn't introduce notions of REWRITING and stuffs -- because Agda wants to have a general notation of custom reduction rule, and Arend focus on HoTT. The underlying type theory is called HoTT-I by the author.