The Coq mailing list

[Todd Wilson <twilson AT csufresno.edu>]

Thanks Daniel, Bas, Benedikt, Ryan, and Vladimir, for the responses so
far; a few words of clarification.

I am concerned about "extra axioms", because my main goal is to
certify (by computer) that a particular construction and associated
line of reasoning is valid in an arbitrary elementary topos.
Therefore, the shallow embedding of Geuvers that Ryan mentions will
probably not be suitable, unless it is easy to see that I've not used
any of the "proves more" part of the embedding. Nor, it seems, could I
use a theory that included Univalence, again unless it were easy to
see that I've avoided it in my construction and proof. I'll have to
look at these embeddings and the formulation of IZF in Coq to see if
the topos-fragment is easily separable.

--Todd


On Tue, Mar 18, 2014 at 6:24 AM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> 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!
>>
>



-- 
Todd Wilson, PhD
Department of Computer Science
California State University, Fresno