The Coq mailing list

[Todd Wilson <twilson+ AT cs.cmu.edu>]

Dear Coq-club members:

I have no experience with Coq, and I am not (yet) a regular reader of 
this mailing list, but I would like to ask about the suitability of Coq 
for a formalization project I am contemplating, and I am hoping that I 
can get some advice from you.  Searches of the archive of this mailing 
list did not turn up any relevant posts.

I published a paper in the Journal of Symbolic Logic (66(3), 1121-1126, 
2001) that showed that Zermelo's proof of AC => WO could be modified so 
that it becomes intuitionistically valid -- at least in the sense that, 
suitably formalized, it holds in the internal logic of any elementary 
topos -- and I would like to formalize and check this proof.  Topos 
logic is a higher-order extensional intuitionisitic logic, and looking 
over the on-line documentation for Coq, it seems that this logic might 
be embeddable into Coq + "Extensionality of Predicates", with Prop 
playing the role of the subobject classifier, Omega.  I also note that 
the "Axiom of Unique Choice" already follows from topos logic, and, 
since proofs are not objects in topos logic, it may be that "Proof 
Irrelevance" is also true (or at least relevant!).

Which leads to my two questions:

(1)  Has anyone actually verified this embedding or something like it? 
That is, has anyone defined an embedding of the language of topos logic 
into the language of Coq and shown that there is a particular Coq theory 
that corresponds exactly to the theory of toposes?

(2)  Assuming that such an embedding and theory exist, has anyone 
identified those portions of the Standard Library that are conservative 
over this theory?

With an answer to (1), I would know that proving a suitably-defined 
version of my theorem in Coq would amount to checking the theorem in my 
paper, and with an answer to (2), I would know exactly what extra 
resources of Coq I could use in proving this theorem and still be 
assured that I was verifying its provability in topos logic.

Thanks,

Todd Wilson