Author Archives: favonia

Covering Spaces

Posted on 27 April 2013 by favonia

Covering spaces are one of the important topics in classical homotopy theory, and this post summarizes what we have done in HoTT.  We have formulated the covering spaces and (re)proved the classification theorem based on (right) -sets, i.e., sets equipped with … Continue reading →

Posted in Code, Higher Inductive Types, Homotopy Theory | 5 Comments

Running Spheres in Agda, Part II

Posted on 11 February 2013 by favonia

(Sorry for the long delay after the Part I of this post.) This post will summarize my work on defining spheres in arbitrary finite dimensions (Sⁿ) in Agda. I am going to use the tools for higher-order paths (discussed in … Continue reading →

Posted in Code, Higher Inductive Types | Leave a comment

Running Spheres in Agda, Part I

Posted on 7 August 2012 by favonia

Running Spheres in Agda, Part I Introduction Where will we end up with if we generalize circles S¹ to spheres Sⁿ? Here is the first part of my journey to a 95% working definition for arbitrary finite dimension. The 5% … Continue reading →

Posted in Code, Higher Inductive Types | Leave a comment