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 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 > > Sent: Monday, February 27, 2017 7:53 PM > To: Thierry Coquand > Cc: Prof. Vladimir Voevodsky; 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 > wrote: >> >> >>> On Feb 25, 2017, at 2:19 PM, Thierry Coquand > 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 . > For more options, visit https://groups.google.com/d/optout .