The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hi,

but definition of a topos itself does not require the assumption that the 
underlying category is univalent, right?

Even less does it require the Univalence Axiom, right?

Vladimir.


On Mar 18, 2014, at 3:22 AM, Benedikt Ahrens 
<benedikt.ahrens AT gmx.net>
 wrote:

> 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!
>