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