Monthly Archives: February 2013

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