One possible way to find a computational interpretation for univalence is to interpret it in using realizability. Stekelburg provides a univalent universe of modest Kan complexes.
Wouter Stekelenburg, Realizability of Univalence: Modest Kan complexes, arXiv
Revision on March 14, 2015 at 16:59:43 by Bas Spitters. See the history of this page for a list of all contributions to it.