The Coq mailing list

[Benedikt Ahrens <benedikt.ahrens AT gmx.net>]

Hi,

I have been thinking about implementing toposes in Coq augmented by the 
Univalence Axiom (i.e. in the Univalent Foundations).
The basic examples of toposes are, in particular, univalent categories 
(see [1], there just called "categories"), which are categories where 
isomorphism of objects coincides with their equality, thus it would make 
sense to define a topos to be univalent in that context.
One could then use Coq's notation mechanism and tactics language to get 
a kind of internal language of a topos in Coq.

Starting out with just the necessary properties of a topos and deducing 
the rest would probably take quite a long time, but if you are willing 
to define a topos to have all these properties, you could get started 
quite quickly going this way. One could replace the axioms by proofs of 
those properties later.

Best,
Benedikt

[1] http://arxiv.org/abs/1303.0584

On 03/17/2014 08:26 PM, Todd Wilson 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!