the scandinavian logic society

slideshow 1

Type theory and univalent foundations

Voevodsky's page: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html

Univalent foundation wiki: http://uf-ias-2012.wikispaces.com/

In particular, the book: http://uf-ias-2012.wikispaces.com/The+book

A temporary copy can be found at: www.cse.chalmers.se/~coquand/BOOK/main.pdf

Article "An intuitionistic theory of types": http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.131.926

Book on Intuitionistic Type Theory: http://www.csie.ntu.edu.tw/~b94087/ITT.pdf

"Isomorphism is equality", N.A. Danielsson and T.C.: http://www.cse.chalmers.se/~nad/publications/

Talks by Mike Shulman: http://www.math.ias.edu/~mshulman/papers/index.html

Talks by Dan Licata: http://www.cs.cmu.edu/~drl/pubs.html

Tutorial by A. Pelayo and M.A. Warren: http://arxiv.org/pdf/1210.5658v1.pdf

Documents available at: http://homotopytypetheory.org/

 Photo of Mount Akka / Àhkka massif seen from the high plateau Maukojaureh north-east of it by Tobias Radeskog / CC BY 3.0.