So the answer was yes, right? Problem solved?

On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:

Just a thought… Can we devise a version of the HTS where exact equality types are not available for the universes such that, even with the exact equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this should be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not be available for them either.