Coq's "singleton elimination" principle and Prop-valued equality

[Peter LeFanu Lumsdaine]

Does anyone know any references on Coq/CIC's "singleton elimination"
principle? I haven’t managed to find anywhere giving a theoretical
discussion of it.

Background: This seems to be the crucial point where Coq’s Prop-valued
equality diverges from the homotopy-theoretic picture. Simply having
a “Prop-valued equality” is fine, as far as I understand — for
instance, if we have bracket types / hProp-reflection, then applying
them to the path types gives an hProp-valued equality. However, one
should then be able to eliminate out of this only into other hProps.
Coq’s main rules for inductive types agree with this: if you define an
inductive Prop, you can only eliminate it into other Props. But
there’s a special exception for empty and “singleton” types (4.5.4 in
the manual, p.118) — eg falsehood, conjunction, and equality — from
which you’re allowed to eliminate into any sort.

A restricted version of this principle (covering falsehood and
conjunction but not of course equality) is provable when Prop :=
HProp. In the original CIC, as far as I can see, these aren’t
provable, but I’m not at all sure — does anyone know more about this?

According to the Coq manual, it was introduced by Paulin-Mohring for
version 7 in 2002; but I haven’t been able to find further references.

Thanks,
–p.

[Vladimir Voevodsky]

There is another important place where singleton elimination is used namely in the use of the "accessibility predicate" Acc ( see http://coq.inria.fr/stdlib/Coq.Init.Wf.html ) .

Vladimir.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To post to this group, send email to HomotopyT...@googlegroups.com.
> To unsubscribe from this group, send email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/HomotopyTypeTheory?hl=en.
>

[Bas Spitters]

There is some discussion on its (problematic) consequences on extraction here:
http://www.springerlink.com/content/3114f6rp11b5qg24/
http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf

Interestingly, in Christine's thesis(1996) eq has type A->A->Set, p70:
http://www.lri.fr/~paulin/PUBLIS/habilitation.ps.gz
On p86, there is a discussion on singleton elimination, with the
apparent justification that it is sound for extraction.

Apparently, it was introduced already in 5.10, p71.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.48.7859&rep=rep1&type=pdf

In any case, I believe the justification to be `this works for
extraction'/ holds in the realizability interpretation.

Best,

Bas