The Univalent Foundations Program [Aczel, Peter; Ahrens, Benedikt; Altenkirch, Thorsten; Awodey, Steve; Barras, Bruno; Bauer, Andrej; Bertot, Yves; Bezem, Marc; Coquand, Thierry; Finster, Eric; Grayson, Daniel; Herbelin, Hugo; Joyal, Andre; Licata, Dan; Lumsdaine, Peter; Mahboubi, Assia; Martin-Lof, Per; Melikhov, Sergey; Pelayo, Alvaro; Polonsky, Andrew; Shulman, Michael; Sozeau, Matthieu; Spitters, Bas; van den Berg, Benno; Voevodsky, Vladimir; Warren, Michael; Zeilberger, Noam; Angiuli, Carlo; Bordg, Anthony; Brunerie, Guillaume; Kapulkin, Chris; Rijke, Egbert; Sojakova, Kristina; Avigad, Jeremy; Cohen, Cyril; Constable, Robert; Curien, Pierre-Louis; Dybjer, Peter; Escardo, Martín; Hou, Kuen-Bang; Gambino, Nicola; Garner, Richard; Gonthier, Georges; Hales, Thomas; Harper, Robert; Hofmann, Martin; Hofstra, Pieter; Kock, Joachim; Kraus, Nicolai; Li, Nuo; Luo, Zhaohui; Nahas, Michael; Palmgren, Erik; Riehl, Emily; Scott, Dana; Scott, Philip; Soloviev, Sergei] Homotopy type theory. Univalent foundations of mathematics. (English) Zbl 1298.03002 Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press. ix, 468 p. (2013). Reviewer: Marco Benini (Buccinasco) MSC: 03-02 55-02 03B15 03G30 18A15 18B05 55U40 PDFBibTeX XMLCite \textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002) Full Text: arXiv Link
Awodey, Steve (ed.); Garner, Richard (ed.); Martin-Löf, Per (ed.); Voevodsky, Vladimir (ed.) Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011. (English) Zbl 1242.00037 Oberwolfach Rep. 8, No. 1, 609-638 (2011). MSC: 00B05 03-06 55-06 03B15 55Pxx PDFBibTeX XMLCite \textit{S. Awodey} (ed.) et al., Oberwolfach Rep. 8, No. 1, 609--638 (2011; Zbl 1242.00037) Full Text: DOI