The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I have the dream to formalize poset/lattice theory in Coq. (I am not very 
qualified yet, but the dream exists.)

My first attempt was based on using GAIA: 
http://www-sop.inria.fr/marelle/gaia/ which is basically an ZFC formalization 
in Coq.

But I noticed that it is handy to treat [sub] as a partial order. This does 
not work in ZFC because proper classes issues.

So I have thought to replace a ZFC binary relation defined in GAIA with just 
[Set*Set->Prop] (or more generally [T1*T2->Prop]).

I doubt whether I can formulate order theory statements without using ZFC.

For example, I was told that Coq's way is to use setoids.

Can reasonable amount of set theory be expressed without resorting to ZFC, 
instead using setoids and other Coq ways? I speak specifically about 
formalization of order theory (partial order, meets, joins, maximum, minimum, 
infimum, supremum, Galois connections, etc.)

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