Mere propositions and propositional truncation

A type is a mere proposition when any two of its elements are equal. This condition permits the type to be empty; adding an inhabitant makes it contractible. A set, in the homotopy-type-theoretic sense, instead has identity types that are mere propositions. Natural numbers and Booleans are sets with many possible elements, rather than mere propositions. This terminology concerns the structure of identity, not a universal declaration that every type is an ordinary set.

Proof irrelevance for mere propositions means that different evidence of the same mere statement cannot be distinguished by an internal function. It does not collapse all witnesses in an arbitrary dependent sum. For a predicate R on a set A, the pair type containing an a and evidence of R can still have several distinct first components. To express only that some such a exists, one can apply propositional truncation to the whole pair type.

Propositional truncation supplies a map sending each element of A to its mere inhabitation and ensures that the resulting type is a mere proposition. Its basic nondependent recursor takes a function from A into a mere proposition P and extends it to a function from the truncation into P. To use the rule, the target's proposition condition is part of the required input. Dependent elimination has the corresponding proposition-valued fiber requirement.

This restriction is not a ban on every function from a truncation into a nonpropositional type. A constant function to a previously known natural number is perfectly definable. The restriction is that one cannot invoke this recursor with an arbitrary target and expect it to preserve different witness-dependent outputs. More refined factorization arguments require extra coherence data. Merely calling the target a set is weaker than calling it a mere proposition and does not discharge the basic recursor's hypothesis.

Suppose R is proposition valued on a set A and any two objects satisfying R are equal. Then the dependent sum of an object and its R certificate is itself a mere proposition: equality of first components follows from uniqueness, and transported certificates agree because R is proposition valued. Its truncation can therefore be eliminated back into that very pair type. Projecting the recovered pair returns the uniquely characterized object. This is unique choice, not a procedure for selecting among arbitrary distinct candidates.

Finite data can also provide an independent construction. If a finite relation is decidable and a witness is known to occur in its explicit search list, an algorithm can inspect that list and return the first verified witness. The extraction then relies on the enumeration, decisions, and termination argument. It does not show that truncation has secretly retained a recoverable first witness, nor that every merely inhabited infinite fiber admits such a search procedure.