The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

On 05/06/2013 11:22 AM, Arnaud Spiwack wrote:

The normal method in Coq is indeed to define a setoid equality on lists.

Is there a good reference using this technique or
should I cite this as folklore?

I don't think there is anything specific. Setoids as a way to do mathematics go back to Bishop's 1967 book Foundations of constructive analysis (although he didn't call them that way). It is a common way conduct mathematics in Coq. Or in a constructive setting in general. The current implementation of so-called setoid rewriting in Coq is due to Matthieu Sozeau (see A New Look at Generalized Rewriting in Type Theory).

An alternative method of defining quotient has been played with in the recent month within the framework of homotopy type theory: higher inductive type (in which case it would work nicely with Coq's native equality rather than a setoid equality). It is not available in Coq yet (though I understand there is a prototype out there).

Let me understand some things:

 * The identity type of HTT would then be a new proof-relevant
   propositional equality type in Coq, while the definitional equality
   stays the same?
 * This new equality will not be an automated Leibniz equality and
   people want to write out substitution "transport" explicitly
   (because of proof-relevance)?
 * If this is true, the identification of constructor terms will only
   be possible by manual application of the equality proofs? Is that
   not worse than using rewriting with a setoid equality? The benefit
   over using setoid equality will therefore only be that functions
   over the higher inductive type are automatically invariant under
   homotopic transport?

Well, you shouldn't focus on the proof relevance thing. It's not relevant to this particular application. All in all, it would be pretty much like the setoid situation, but internalised within the native equality. Resulting in a lot fewer proofs obligations to be discharged by the user, and much smaller proof terms.
 

Is there some writeup of the Coq extension yet?
Alternatively I would like to name the (future) implementors of
this Coq extension and not just point to the homotopy blog.

None that I know of. And I've just heard of the prototype, I don't know who wrote it.

I forgot another approach to quotient, a bit like what Moca does, but without the automation. The idea is that if you have a notion of canonical form, and a test for canonicity the (dependent) type { x:A | canonical x = true } happens to be a quotient (in fact a retraction) of A for the equality of Coq, without any proof obligations to prove ever. It's been perused in Cyril Cohen's PhD. That sounds more like in the spirit of what you are trying to do.


I'm not aware of any work that would try to change definitional equality to achieve this sort of quotients.