The Coq mailing list

[Todd Wilson <twilson AT csufresno.edu>]

Hi, all:

Does anyone have a library or set-up that exactly captures the logic
of elementary toposes? I'm looking for a way to prove theorems in an
interactive environment, ideally Coq, so that I'd know that all of the
theorems I'd proven are true in every elementary topos. Even better
would be to have the ability to extract terms in any one of the
several equivalent languages of elementary topos theory witnessing the
theorems I prove. Thanks!

Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh