Is 'subsingleton elimination' the same concept as 'function comprehension'?

Question

I saw:

• subsingleton elimination from lean-forward, which, I so far understood as "eliminate a type in Prop to a type in whatever universe that we know has at most one constructor with arguments either in Prop or also subsingletons".
• function comprehension from XTT, $\S 8.2.1$, which corresponds to the statement that (paraphrased) if ∀ (a : A), ∃ (b : B), R a b ∧ b unique, then ∃ f : A -> B, it holds that ∀ (x : A), R x (f x). If A lives in Type then this is trivial, but when A : Prop then this becomes more interesting: we intend to erase propositions, so we cannot have their computational content relevant, so only when we know b unique do we say ∀ x, f x = b.

I wonder are these concepts the same thing? Is there any slight difference I didn't notice? They're both about eliminating Prop into some uniquely inhabited Type.

Answer 1

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.