Re: [HoTT] about the HTS

[Benedikt Ahrens <benedik...@gmail.com>]

On 02/23/2017 03:47 PM, Vladimir Voevodsky 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.


Paolo Capriotti, in his PhD thesis "Models of Type Theory with Strict
Equality" [1], has studied strict equality in type theory.

From page 69:

"Finally, universes in the strict fragment of our system are not assumed
to be fibrant types, like in HTS."

You might be interested in Section 4.1.1, "Differences with HTS".

[1] https://arxiv.org/abs/1702.04912