Author Archives: Dan Licata

The torus is the product of two circles, cubically

Back in the summer of 2012, emboldened by how nicely the calculation π₁(S¹) had gone, I asked a summer research intern, Joseph Lee, to work on formalizing a proof that the higher-inductive definition of the torus (see Section 6.6 of the HoTT book) … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 31 Comments

Homotopical Patch Theory

This week at ICFP, Carlo will talk about our paper: Homotopical Patch Theory Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper Homotopy type theory is an extension of Martin-Loef type theory, based on a correspondence with homotopy theory and higher category … Continue reading

Posted in Uncategorized | 4 Comments

Eilenberg-MacLane Spaces in HoTT

For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … Continue reading

Posted in Applications, Code, Higher Inductive Types, Paper, Univalence | 6 Comments

Another proof that univalence implies function extensionality

The fact, due to Voevodsky, that univalence implies function extensionality, has always been a bit mysterious to me—the proofs that I have seen have all seemed a bit non-obvious, and I have trouble re-inventing or explaining them.  Moreover, there are … Continue reading

Posted in Univalence | 4 Comments

New writeup of πn(Sn)

I’m giving a talk this week at CPP.  While I’m going to talk more broadly about applications of higher inductive types, for the proceedings, Guillaume Brunerie and I put together an “informalization” of πn(Sn), which you can find here. This is … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 1 Comment

Homotopy Theory in Type Theory: Progress Report

A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic tools used in our synthetic approach … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 13 Comments

Homotopy Theory in Homotopy Type Theory: Introduction

Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this … Continue reading

Posted in Applications, Higher Inductive Types, Homotopy Theory, Uncategorized, Univalence | 3 Comments