The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am studying Coq and maybe now may attempt a practical exercise of writing 
some theories.

I noticed that the Coq approach is to use setoids. In my opinion, it is silly 
and contrary to what we do in informal mathematics.

On the other hand we have a ZF(C) formalization:
See a .tar file with the theory at:
http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1
from the article:
http://arxiv.ccsd.cnrs.fr/abs/math/0402336v1

In Isabelle the development of was split into Isabelle/HOL and Isabelle/ZF 
which cannot interact with each other. That's somehow bad.

On the contrary in the above mentioned ZF formalization for Coq can be used 
together with the rest Coq theories because a set is just a type.

So, I'm declined to write based on ZF.

Can anyone give me any arguments (against or for)?

-- 
Victor Porton - http://portonvictor.org