## 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. Simplicial homotopy theory can be developed in an [[nlab:extensive]] [[nlab:locally cartesian closed]] category $A$. Such categories are also called [[nlab:Heyting bialgebras]]. The category $A$ has a class of [[nlab:small maps]] which has a bundle of small [[nlab:assemblies]]. This provides an internal [[nlab:Heyting bialgebra]] $S$ which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets. Within $S$ we can define a universe $M$ and show that it is fibrant. This universe is even univalent. Now, the category of assemblies in number realizability provides such a Heyting bialgebra. The modest sets, a small internally complete full subcategory, provide the univalent universe. Note that modest sets are an [[nlab:impredicative]] universe. It models the [[nlab:calculus of constructions]]. ## References Wouter Stekelenburg, _Realizability of Univalence: Modest Kan complexes_, [arXiv](http://arxiv.org/abs/1406.6579)