Calculating the fundamental group of the circle in homotopy type theory. Dan Licata and Michael Shulman, LICS 2013,
http://www.cs.cmu.edu/~drl/pubs.html
arXiv:1301.3443