The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi,

I am looking for examples of the use of Coq's "singleton elimination"
feature for eliminating out of inductive Props into non-Prop types.
The canonical examples seem to be equality 'eq' and the accessibility
predicate 'Acc' used in defining wellfoundedness.  I guess there are
also True, False ("singleton elimination" also applies to inductive
Props with no constructors), and the conjunction of two propositions.
I would be interested to hear of any other examples, from any source.

(Context: under a homotopical interpretation, if Prop were to be
replaced by a universe of h-propositions, then singleton elimination
would no longer be valid for 'eq' (except over domains that are
h-sets), but it would still be valid for 'Acc' and for the more
trivial examples.  It would be nice to have more examples against
which to test a general principle of which singleton eliminations
remain valid.)

Thanks!
Mike