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
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
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
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
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
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
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
Abstract Types with Isomorphic Types
Here’s a cute little example of programming in HoTT that I worked out for a recent talk. Abstract Types One of the main ideas used to structure large programs is abstract types. You give a specification for a component, and … Continue reading
A Simpler Proof that π₁(S¹) is Z
Last year, Mike Shulman proved that π₁(S¹) is Z in Homotopy Type Theory. While trying to understand Mike’s proof, I came up with a simplification that shortens the proof a bunch (100 lines of Agda as compared to 380 lines … Continue reading
Canonicity for 2-Dimensional Type Theory
A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading
Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute
Higher-dimensional inductive types are an idea that many people have been kicking around lately; for example, in An Interval Type Implies Function Extensionality. The basic idea is that you define a type by specifying both what it’s elements are (as … Continue reading
Just Kidding: Understanding Identity Elimination in Homotopy Type Theory
Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP … Continue reading
A Formal Proof that the Higher Fundamental Groups are Abelian
Homotopy type theory (HoTT) will have applications for both computer science and math. On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, … Continue reading
Homotopy Type Theory 