Re: [UniMath] [HoTT] about the HTS

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

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

We also validate axiom K with the hSet, as far as I understand.

BTW why do you call elements of bSet Bishop sets?


> On Feb 27, 2017, at 1:58 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:
> 
> 
> Exactly.
> 
>  In my note, I consider three universes (all fibrant)
> 
>  sProp 
>  sSet
>  bSet
> 
>  sProp sub-presheaf of sSet sub-presheaf bSet sub-presheaf U
> 
>  They correspond to 3 properties
> 
>  G |- A sprop
>  G |- A sset
>  G |- A bset
> 
> that can be described semantically in a simple way.
> 
>  For sprop and sset, to have a fibration structure is a property
> and 
> 
>  G |- A sset and fibrant
> 
> should correspond to the notion of covering space.
> 
>  But sSet does not correspond to a decidable type system, while
> it should be the case that sProp and bSet corresponds to a decidable
> type system.
> 
>  At least with bSet we validate axiom K and all developments that have
> been done using this axiom.
> 
> 
> 
> 
> From: Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>>
> Sent: Monday, February 27, 2017 7:53 PM
> To: Thierry Coquand
> Cc: Prof. Vladimir Voevodsky; univalent-...@googlegroups.com <mailto:univalent-...@googlegroups.com>; homotopytypetheory
> Subject: Re: [UniMath] [HoTT] about the HTS
>  
> BTW, even if the universe of strict sets is not fibrant we can still have a judgement that something is a strict set and the rule that a = b implies a is definitionally equal to b if a and b are elements of a strict set.
> 
> It is such a structure that would make many things very convenient. 
> 
> It is non- clear to, however, why typing would be decidable in such a system.
> 
> Vladimir.
> 
> 
> 
> 
>> On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>> wrote:
>> 
>> 
>>> On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote:
>>> 
>>>  “Bishop set” which corresponds
>>> to the fact that any two paths between the same end points are -judgmentally- equal.
>> 
>> This is not what I mean by a strict set. A strict set is a Bishop set where any two points connected by a path are judgmentally equal.
>> 
>> 
> 
> -- 
> 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 #2: Type: text/html, Size: 12430 bytes --]