coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq-Club Club <coq-club AT inria.fr>, homotopytypetheory AT googlegroups.com
Subject: [Coq-Club] an update to "Univalent Foundations"
Date: Tue, 17 May 2011 10:29:39 -0400

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