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