Re: [HoTT] about the HTS

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

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

 Here is note <http://www.cse.chalmers.se/~coquand/bishop.pdf> which should be connected to this message. It contains first a self contained
presentation of the cubical set model, and then a notion of “Bishop set” which corresponds
to the fact that any two paths between the same end points are -judgmentally- equal.
One defines a subpresheaf of the universe which classifies these sets, and  one notices
that this notion is closed by the Kan filling operation of the universe (because this is defined
in term of glueing, and this notion is closed by the glueing operation), and hence it is fibrant
(and univalent).

 If this is correct, one expects a corresponding type system with decidable type-checking, and
connections with what has
been done in observational type theory (and it will be interesting to see if this can also be connected
to the more recent work of Thorsten et al.) while staying in a univalent theory.
 Thierry


On 23 Feb 2017, at 15:47, Vladimir Voevodsky <vlad...@ias.edu<mailto:vlad...@ias.edu>> 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: 2906 bytes --]