Re: [HoTT] about the HTS

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

BTW It is a little dangerous to define presheaves as functors C -> Sets^{op}. While it gives the correct objects, the morphisms between presheaves are not morphisms in the category of functors C -> Sets^{op} but in the opposite category.


> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens <benedik...@gmail.com> wrote:
> 
> 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.
>> 
> 
> -- 
> 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.