The Coq mailing list

[Victor Porton <porton AT narod.ru>]

05.11.2011, 21:02, "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?

Oh, I noticed that the work 2 is based on 1. So I expect that 2 is better 
than 1.

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