Toward a Computational Interpretation of Univalence