The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

My first thought would be to set up the language and axioms of a
topos.  Encoding it as a subset of Coq would be tricky, as a topos
doesn't necessarily have an object corresponding to Type, and it
definitely doesn't have an object corresponding to nat in general.  So
maybe, depending on how you want to go, start off with some objects
like Hom, id, comp, prod, pi1 : Hom (prod A B) A, pi2, prod_map : Hom
A B -> Hom A C -> Hom A (prod B C), equalizer, P, Sub, equivalence
maps between Hom A (P B) and Sub (prod A B), etc.  And then specify
enough relations to make them into what you'd expect.

I don't know about extracting proofs into a language of topos theory.
-- 
Daniel Schepler

On Mon, Mar 17, 2014 at 12: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