Re: [HoTT] about the HTS

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

Section 1.4.8 "Equality" gives an informal account and points to several
precise definitions.
On page 43 two equality types are considered, one intensional one and
one with reflection rule.

Maybe Paolo (in CC) can explain his setup himself.

On 02/23/2017 07:08 PM, Vladimir Voevodsky wrote:
> 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.
>