Author Archives: avigad
Another Formal Proof that the Higher Homotopy Groups are Abelian
I have adapted Dan Licata’s Agda proof that the higher homotopy groups are abelian to Coq, and I have added a link to the code on the code page of this blog.
Posted in Code
4 Comments
Homotopy Type Theory 