3 ms·
Right; indeed they have _definitionally_ at most one inhabitant. Swiping the following spec from the page you link: Definition irrelevance (A:SProp) (P:A ->
by ocfnash 7y ago
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.