Re: [HoTT] about the HTS

[Vladimir Voevodsky <vlad...@ias.edu>]

I could not find where he defines the univalent (intensional) equality. It seems that all his equalities are strict.


> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens <benedik...@gmail.com> wrote:
> 
> 
> 
> 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
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.