_Eilenberg-MacLane Spaces in Homotopy Type Theory_. [[Dan Licata]] and [[Eric Finster]], LICS 2014 ## Links ## [http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda)