The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

If you try to shallowly embed higher order logic (the internal language of a 
topos) into Coq, it turns out that the Coq encoding proves more theorems than 
HOL.  This translation and a discussion of its properties can be found in

The Calculus of Constructions and Higher Order Logic
Herman Geuvers
1992

Ryan

On Mar 17, 2014, at 3:26 PM, Todd Wilson 
<twilson AT csufresno.edu>
 wrote:

> 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