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 <vl...@ias.edu>
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 <vlad...@ias.edu> wrote:

On Feb 25, 2017, at 2:19 PM, Thierry Coquand <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.