The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> actually in 8.3pl2 rewrite works with "identity" - a version of paths which 
> is defined in Coq.Init. It does not work with "paths" defined separately, 
> but if you define "paths" (as I do in the latest version of my library) as 
> a notation for "idenity" then rewrite works with it.

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.

With kind regards,

Andrej