I am familiar with the basics of coq. What does the new SProp sort do? I couldn't understand the docs.

Were you able to find this doc [0]? As best I understand it, a Prop P has as many inhabitants as there are proofs of P, whereas an SProp S has at most one inhabitant, according to whether it is true or not. All proofs of S are declared to be "the same". (Convertible is the word they use.)

[0] https://coq.github.io/doc/v8.10/refman/addendum/sprop.html

Right; indeed they have _definitionally_ at most one inhabitant. Swiping the following spec from the page you link:

  Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.

the point is that `irrelevance` consumes an inhabitant `v` of the Prop `P x` and is supposed to "return" an inhabitant of the Prop `P y`. A priori `P x` and `P y` are different types but since `x` and `y` are both inhabitants of a type whose sort is `SProp`, they are definitionally equal and so `v` is definitionally a valid inhabitant of `P y`. This justifies the implementation of `irrelevance` as `v`.

I can imagine some other illustrative examples but I think I'll wait till I've played with SProp to confirm I'm not barking up the wrong end of the stick.