The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am now faced with four choices:

1. To formalize my theory based on ZF theory in Coq by Carlos Simpson: 
http://arxiv.ccsd.cnrs.fr/e-print/math/0402336v1 ;
http://arxiv.ccsd.cnrs.fr/abs/math/0402336v1

2. To formalize my theory based on the theory in Coq by José Grimm: 
http://hal.archives-ouvertes.fr/inria-00408143/ ;
http://hal.archives-ouvertes.fr/inria-00440786/

3. Formalize in Coq's way using setoids (which I don't like for now).

4. To not formalize at all.

The variant 2 has the advantage over the variant 1 in that there the theory 
of poset and lattices is already formalized. But that advantage is void 
because in 2 posets and lattices are formalized without use of type classes, 
and one needs to rewrite it anyway.

What of the four variants you'd suggest? Particularly is 1 or 2 a better 
theory, how do they compare?

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