## Idea One possible way to find a computational interpretation for univalence is to interpret it in using [[nlab:realizability]]. Stekelburg provides a univalent universe of modest Kan complexes. ## References Wouter Stekelenburg, _Realizability of Univalence: Modest Kan complexes_, [arXiv](http://arxiv.org/abs/1406.6579)