(Link)

Authors: Kuen-Bang Hou (Favonia) (Carnegie Mellon University), Eric Finster (École Polytechnique), Daniel R. Licata (Wesleyan University), and Peter LeFanu Lumsdaine (Stockholm University)

Reference: Hou, K. B., Finster, E., Licata, D. R., & Lumsdaine, P. L. (2016). A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. In Proceedings of the 31st annual ACM/IEEE symposium on logic in computer science (LICS 2016) (pp. 565-574)

Why this paper? Cited by Automating Boundary Filling in Cubical Agda and Strange new universes: Proof assistants and synthetic foundations

I first became aware of this paper from a long and fascinating blog comment thread in which mathematicians argued about the utility, or lack thereof, of homotopy type theory for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying “it was remarkable to see a complete homotopy theory newbie, who had the proof in HoTT, explain it to none less than Charles Rezk, who said he had tried to find it using traditional means but failed”.

This paper occupies the same genre as the Brunerie thesis I read about a year ago, as it re-proves a known homotopy theoretic result (this one from the 1950s) in synthetic style using type theory. Because of the synthetic treatment, the result is transferrable to any ∞-topos (this generality is what is heralded as ‘new’ in the Schreiber quote above). Like Brunerie’s work, the proof is “essentially new” rather than merely a translation of existing work to a different language. Unlike Brunerie’s work, which was a tour de force of pen-and-paper type theory, this work is entirely formalised, using the proof assistant Agda.

I was familiar going into this paper about the notion of truncation. In type theory one has identities between elements, but because identities are themselves elements of an identity type, one also has identities between identities, and so forth. A type is n-truncated, or simply an n-type, if at every level above n the identities are trivial. For example a set is a 0-type, as while it may be non-trivial at level 0 (some sets have multiple elements which are not equal) it is trivial above that level (there is only one way for an element to be equal to itself). Connectivity is the dual notion to truncation: elements are trivial below a certain level. This extends to connectivity of a map between types; to say that such a map is n-connected is to (very roughly) say that it shows the two types to be equivalent up to level n.

The Blakers–Massey theorem is about the connectivity of certain maps used in the definition of a pushout, a construction similar to a disjoint union but also featuring some ‘glue’ that joins some elements together. The canonical example is defining the integers as two copies of the natural numbers glued together at their zeros. The theorem is apparently greatly useful for describing the algebraic structure of the higher levels of some examples in homotopy theory, which in general is an extremely hard problem.  This paper in fact offers two proofs, one more homotopy theory flavoured version which goes via a detour through a special case of pushout called a wedge, the other a more type theoretically pure version that avoid this detour, which is slightly shorter but more reliant on computations which are hard to explain on paper.