Re: [UniMath] [HoTT] about the HTS

[Thierry Coquand <Thierry...@cse.gu.se>]

> We also validate axiom K with the hSet, as far as I understand.
> 
> BTW why do you call elements of bSet Bishop sets?

 If G |- A is a fibration and A is a strict set then the fibers over any point
can be thought of as ordinary sets (all paths are constant paths), and we have unique path lifting
property (like for covering space).
 
 If G |- A is a fibration and A is a “Bishop” set, then the fibers over any
point can be thought of as graphs of equivalence relations
(the paths don’t need to be constant, but there is at most one
path between two points, and more generally all cubes are determined
by its vertices).
This is quite close to how Bishop defined a set: a set is defined
by a collection of elements with an equivalence relation.
If we furthermore look at a fibration of “Bishop” sets this corresponds
exactly to the notion of family of sets as defined by Richman
in his book on constructive algebra (or in the book by Bishop and
Bridges Exercise 3.2).

 In any case, both notions of strict sets and “Bishop” sets
give rise to sub-presheaves of the first universe and we have sSet sub-presheaf bSet.
 
 There is also a sub-presheaf of “strict” propositions, which justifies
the rule

    G |- A sProp    G |- a0 : A      G |- a1: A
 ———————————————————
             G |- a0 = a1 : A

(but this type sProp is probably not equivalent in general to the type
of hPropositions)



 Both sSet and bSet should be closed by sum and product types.

  However, they are not closed by quotient (even by propositional truncation)
in general.

   Indeed axiom K is already validated with hSets.

  Maybe the notion of sProp, and bSet is interesting since it should keep conversion
and type-checking decidable, and simplify some proofs, and some computations
by introducing judgmental proof irrelevance (so that we know that we don’t need
to consider some part of a term for computation and conversion).

 In any case, if all this is correct, it is interesting that we can keep some ideas of HTS
(with sSet or bSet) and still be in an univalent framework.

     Thierry