The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Wed, 4 Apr 2012 10:00:33 +0200, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:
> Yes, I noticed that. It actually works with any type that is defined
> just like identity, i.e., you could define your own paths as
> 
>    Inductive paths {A : Type} (x : A) : A -> Type := idpath : paths x x.
> 
> and it would still work exactly the same. It's really nice to have
> rewriting for homotopy type theory.

So, there are two types of rewriting available in coq. The one that is
used for definitions like this, that work by eliminating an inductive
type like that above, and works for terms in arbitrary position (but not
under lambdas).

There is also a setoid based rewriting, that works over arbitrary
(Prop-based) relations, which requires an explicit proof that functions
are Proper with respect to the relation, and which does work under
lambdas. This doesn't work with relations living in Type, since it uses
> Definition relation := A -> A -> Prop.
to identify the type of relations. 
<https://coq.inria.fr/bugs/show_bug.cgi?id=2440>

  Tom