Indeed, these two notions are about what we allow to eliminate from Prop
to Type
, and they both roughly follow the idea that "using propositions to build relevant content is fine as long as there is but one way to use it". But they are quite different.
Subsingleton elimination (in the way this term is usually used) is a syntactic/structural criterion on inductive types, that tells you for which such inductive types pattern-matching/eliminators is allowed with a return type in Type
. This criteria is designed so that there is at most one canonical form of this type, so that there is definitionally at most one inhabitant in the empty context (if canonicity holds).
Function comprehension, on the other hard, is a semantic criterion, which allows to construct a relevant function out of irrelevant content, provided one can show internally that there is but one possible such function. The paradigmatic example of this idea is what the HoTT Book calls principle of unique choice (section 3.9, where they also mention what you call function comprehension as corollary).
The important difference, as highlighted, is that the first notion is syntactic, while the second is semantic. This means that subsingleton elimination is necessarily more restrictive than unique choice/function comprehension, but it has the advantage that it can be checked mechanically, and that in practice it is nice to avoid the whole going-through-unique-choice yoga when you want to eliminate a Prop
inductive into Type
. Moreover, as pointed out by the people working on strict propositions (see my answer to a previous question), the subsingleton criterion might need to be refined/amended depending on the exact kind of propositions you want.
f : A -> B
" but "there exists somef : A -> B
"? $\endgroup$