I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.


I am just curious if there has been any progress towards a computational interpretation of univalence? If not, is the general feeling that univalence is not compatible with computation?



Progress towards a computational interpretation of the univalence axiom?
[Cubical type theory](https://ncatlab.org/nlab/show/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).


