UF IAS 2012 Archive Resources

Some documents for reference.

• Mike Shulman’s coq code for 3 definitions of Id-types.
• Peter Aczel’s slides from a talk.
• Vladimir’s Notes on Type Systems dated 7.23.12.
• Vladimir’s Universe Polymorphism dated 1.11.12 .
• Homotopy type theory and Voevodsky’s univalent foundations by Alvaro Pelayo and Michael A. Warren (includes the corresponding Coq file as an ancillary file).
• Slides from Steve Awodey’s IAS talk on Univalent Foundations.