The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Victor Porton wrote:
> 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.
>    

I suggest thinking hard before trying to do Coq developments that look 
like ZF.  Type theory is an _alternative_ to set theory, and it is much 
more convenient for the sorts of theorems I have experience with.  You 
might find the same for your domain.  You can easily work with sets 
(e.g., ensembles in the Coq standard library) without bringing in ZF.