The loop space of the 2-sphere

Back in January 2016 I gave an introductory talk at the University of Ljubljana about Homotopy Type Theory. The goal of this talk was to display some basic techniques in the field, such as constructing higher inductive types, and using the encode-decode method to figure out what its identity type is. Recall that the topological … Continue reading The loop space of the 2-sphere