coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] an update to "Univalent Foundations"

From: Carlos Simpson <Carlos.Simpson AT unice.fr>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: Coq-Club Club <coq-club AT inria.fr>, homotopytypetheory AT googlegroups.com
Subject: Re: [Coq-Club] an update to "Univalent Foundations"
Date: Tue, 17 May 2011 22:48:50 +0200

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

[Coq-Club] how a client should check a Coq proof for cheating?, Georgi Guninski
- <Possible follow-ups>
- Re: [Coq-Club] how a client should check a Coq proof for cheating?, Bruno Barras
  - Re: [Coq-Club] how a client should check a Coq proof for cheating?, Georgi Guninski
    - Re: [Coq-Club] how a client should check a Coq proof for cheating?, Randy Pollack
  - [Coq-Club] an update to "Univalent Foundations", Vladimir Voevodsky
    - Re: [Coq-Club] an update to "Univalent Foundations", Carlos Simpson
      - Re: [Coq-Club] an update to "Univalent Foundations", Vladimir Voevodsky
        
        Re: [HoTT] Re: [Coq-Club] an update to "Univalent Foundations", Thomas Streicher
        
        Re: [HoTT] Re: [Coq-Club] an update to "Univalent Foundations", Carlos Simpson
        
        Re: [HoTT] Re: [Coq-Club] an update to "Univalent Foundations", Thomas Streicher