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.
>