< [[nlab:homotopy type theory - references]] Currently in the middle of porting these references to the nlab ##Synthetic homotopy theory## * _[[Calculating the fundamental group of the circle in homotopy type theory]]_. [[Dan Licata]] and [[Michael Shulman]], LICS 2013, available [here](http://www.cs.cmu.edu/~drl/pubs.html) and on [arXiv](http://arxiv.org/abs/1301.3443) * _[[$\pi_n(S^n)$ in Homotopy Type Theory]]_, [[Dan Licata]] and [[Guillaume Brunerie]], Invited Paper, CPP 2013, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb13cpp/lb13cpp.pdf) * _[[Homotopy limits in type theory]]_. [[Jeremy Avigad]], [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. [arXiv](http://arxiv.org/abs/1304.0680) * _[[Eilenberg-MacLane Spaces in Homotopy Type Theory]]_. [[Dan Licata]] and [[Eric Finster]], LICS 2014, [PDF](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda) * _[[A Cubical Approach to Synthetic Homotopy Theory]]_. [[Dan Licata]] and [[Guillaume Brunerie]], LICS 2015, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * _[[Synthetic Cohomology in Homotopy Type Theory]]_, [[Evan Cavallo]], [PDF](http://www.cs.cmu.edu/~rwh/theses/cavallo.pdf) * _[[A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory]]_, LICS 2016 [[Kuen-Bang Hou (Favonia)]], [[Eric Finster]], [[Dan Licata]], [[Peter LeFanu Lumsdaine]], [arXiv](http://arxiv.org/abs/1605.03227) * _The Seifert-van Kampen Theorem in Homotopy Type Theory_, [[Kuen-Bang Hou]] and [[Michael Shulman]], [PDF]( http://www.cs.cmu.edu/~kuenbanh/files/vankampen.pdf) * _[[On the homotopy groups of spheres in homotopy type theory]]_, [[Guillaume Brunerie]], Ph.D. Thesis, 2016, [arxiv](https://arxiv.org/abs/1606.05916) * _[[The real projective spaces in homotopy type theory]]_, [[Ulrik Buchholtz]] and [[Egbert Rijke]], LICS 2017, [arxiv](https://arxiv.org/abs/1704.05770) * _[[Covering Spaces in Homotopy Type Theory]]_, [[Kuen-Bang Hou (Favonia)]], [doi](https://doi.org/10.1007/978-3-319-21284-5_15) [[!redirects references]] category: reference, navigation