The Coq mailing list

[Andreas Schropp <schropp AT in.tum.de>]

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?

> 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?


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.

Thanks,
  Andy