Re: [HoTT] about the HTS

[Thierry Coquand <Thierry...@cse.gu.se>]

[-- Attachment #1: Type: text/plain, Size: 1597 bytes --]


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.


[-- Attachment #2: Type: text/html, Size: 3127 bytes --]