Re: [HoTT] about the HTS

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

[-- Attachment #1.1: Type: text/plain, Size: 2944 bytes --]

1. As Thierry pointed out previously, the problem with sSet is that if we postulate that nat:sSet, then for any (small) type T, the function type T -> nat is in sSet, e.g. nat -> nat is in sSet.

Since it is possible to construct two elements of nat -> nat the equality between which is an undecidable proposition, it implies that the definitional equality in any sufficiently advanced type system with sSet and nat:sSet is undecidable.

That means that witnesses, in some language, of definitional equality need to be carried around and therefore the design of a proof assistant where the proof term is the proof is not possible in this system.

2. It is not so clear what would happen with only bSet and nat:bSet.

Vladimir.





> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
> 
> 
> If my note was correct, it describes in the cubical set model two univalent universes
> (subpresheaf of the first universe)  that satisfy
> 
>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p is the constant path a
> (equality reflection rule)
> 
>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A a b
> (judgemental form of UIP)
> 
>  Maybe (1) or (2) could be used instead of HTS (and we would remain in an univalent
> theory, where all types are fibrant)
> 
>  For testing this, one question is:  can we define semi-simplicial types in (1)? in (2)?
> 
>  Best regards,
>  Thierry
> 
> 
> 
>> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com <mailto:atm...@gmail.com>> wrote:
>> 
>> 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.
>> 
>> --
>> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 5207 bytes --]

[-- Attachment #2: Message signed with OpenPGP --]
[-- Type: application/pgp-signature, Size: 507 bytes --]