The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

On Thu, 27 Nov 2003, Venanzio Capretta wrote:

> The real point in which a canonical representation of some set is better
> than a setoid representation is that equality becomes convertibility.
> That means that we can substitute equal objects in any context. You want
> that (mkRat t1 b1 H1) is convertible with (mkRat t2 b2 H2) if t1 is
> convertible with t2 and b1 with b2. This is not in general true even if
> you have unicity of equality proofs.
> If  you have to prove H1=H2, then it is not better that using a setoid.

Can anyone think of a practical situation when you have t1 and t2
convertable b1 and b2 convertable, but H1 and H2 not convertable.

If t1 t2 b1 and b2 are all closed, it seems likely in practice that H1 and
H2 would be closed too.  If they are not closed, they seem unlikely to be
converable in practice.

-- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.