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> 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.
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.