The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hi Carlos,

my foundations setup is grounded in ZFC through what I call the univalent 
model of type theory. Formalizing this model is an important and interesting 
undertaking.  It can be done in a subset of Coq which does  not use 
universes. This is a whole area of work which has to be done. 

The way I see it one needs first to formalize the language of coq in a much 
more simple type theory and then inside this "decidable" type theory to build 
the required models. 

A non-formal description of  the univalent model can be found on my website 
in "Notes on Type Systems". 

Very best,
Vladimir.


On May 17, 2011, at 4:48 PM, Carlos Simpson wrote:

> Dear Vladimir,
>  Can we do usual ZFC set theory (maybe with one or two Grothendieck-Tarski
> universes) in your foundational setup?
> If so, is there then furthermore a way of relating it to the more
> general types you consider?
> Thanks
> ---Carlos
> 
> 
> Selon Vladimir Voevodsky 
> <vladimir AT ias.edu>:
> 
>> Hello,
>> 
>> I have just posted an update to the "Univalent Foundations" library to my
>> github at https://github.com/vladimirias/Foundations/
>> 
>> The most important new thing in this release is the construction of true
>> set-quotients of types. 
>> 
>> Vladimir.
>> 
>> 
>> 
>> 
>> 
> 
>