Computational Higher Type Theory III: Univalent Universes and Exact Equality