The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The article at http://arxiv.org/abs/math/0311260v2 about a formalization of ;
ZF in Coq contains "and also contains as a tar-attachment to the source file 
the revised and expanded version of the proof development which had been 
attached to math.HO/0311260".

I have seen this .tar file earlier but now cannot find it again. Where is the 
tar with Coq sources?

We need to put a reference to that tar somewhere to Cocorico in order to make 
its finding easier. It is an important, and as it seems to me, a well written 
system of modules. It should be easily findable for visitors of Coq site (now 
it isn't).

----

I am now studying Coq. I want to create a theory of posets, semilattices, 
lattices, and complete lattices.
I consider to base my theory on the above mentioned ZF modules.

Later I may formalize my theory of filters, filtrators, (pointfree) funcoids:

http://www.mathematics21.org/algebraic-general-topology.html

Maybe it's worth to invest into formalizing for absolute certainty of no 
errors in my theorem formulations.

(Or just to formalize for formalization sake).

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