Discussing 'On the homotopy groups of spheres in homotopy type theory'

(Link)

Author: Guillaume Brunerie (Université Nice-Sophia-Antipolis)

Reference: Brunerie, Guillame. “On the homotopy groups of spheres in homotopy type theory.” PhD Thesis, Université Nice-Sophia-Antipolis. 2016

Why this paper? Cited by Formalizing π4(S3)≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda, Commuting Cohesions, and Encoding Dependently-Typed Constructions into Simple Type Theory

Many PhD dissertations are constructed by ‘stapling together’ a variety of different research papers generated during the years of study, with a varying level of effort put into writing connective tissue between them. This is very much not one of those dissertations. Instead, it is a book length development of a single mathematical fact, that π4(S3)≅ℤ/2ℤ. Of course, unpacking this line of mathematics would take time - ‘the fourth homotopy group of the 3-sphere is equivalent to a certain 2-element group’ is a first unpacking, but there is much jargon in there would itself require unpacking – but the focus on this one result is still notable.

I will of course not pretend to do full justice to the multiple years of effort that went into this thesis in the space of a short blog post, but instead try to give some high level feeling for what is going on here. At first glance it is perhaps a bit perplexing; the core result is a well known (although not easy) result in homotopy theory from the 1930s; why is a modern PhD thesis spending hundreds of pages to prove it? The answer is that this a landmark effort within homotopy type theory (HoTT); indeed, it is perhaps the most substantial development of a major result using HoTT. Translating this result into the foundations provided by HoTT turns out to be far from trivial. At one level working within this type theory is helpful, for example obviating the need to ever prove any functions are continuous (well-behaved), because they must be continuous by construction. For example the difficulty of one particularly gnarly part of the standard development, proving that the associativity of the smash product is suitably continuous, simply disappears. Furthermore because the work is ‘synthetic’, in the sense of not being tied to any particular presentation of topology, it is highly general and the core development is not obscured by the particular details of a concrete choice (e.g. working via point-set topology, or simplicial sets).

However, there is a catch: the standard development of results in homotopy theory often contain intermediate constructions that are not well behaved in the sense that HoTT enforces, even where the final product is well behaved. This means that the standard development, at least in this case, cannot be translated line by line into the new formalism as one might naively hope: Brunerie reflects in his superbly reflective concluding chapter that he “often had to find completely different definitions, proofs or statements that would work in homotopy type theory”. The point of all this effort is, of course, not merely to reprove old results, but to pave the way for new advances in homotopy theory (and other areas of mathematics) using HoTT as a tool that avoids certain errors by enforcing certain invariants, in a style amenable to mechanisation.

Having said that, one notable aspect of this development is that it is not mechanised (encoded into a computer), although mechanisation is certainly discussed. This perhaps flies in the face of some people’s intuitions that type theory, resembling as it does a programming language, is innately connected to computer mathematics. Instead this is a significant development of pen and paper type theory, in the 'informal' style recommended by the original HoTT book.

Another interesting aspect of this thesis is its constructivity, and what that means in practice. At the end of chapter 3 it is proved that π4(S3)≅ℤ/nℤ for some integer n. The nature of constructive mathematics is that an existential result of this sort is impossible to prove without generating its ‘witness’; in other words we should have access to the value of the number n (in this case, 2). More precisely, if a witness is not immediately clear from the proof as written, the proof should compute until it produces the witness. This does not happen in this thesis; instead three more chapters are needed to prove that n is in fact equal to 2. What went wrong? One might wonder if the problem is that the proof is pen and paper and hence cannot compute, but although this is part of the problem it is not dispositive: one could try to carry out the computations by hand. Unfortunately these calculations proved too difficult to carry out. An early attempt to develop the thesis within cubical type theory, which is a fully constructive presentation of HoTT which hence would compute, did not prove successful and led Brunerie to conclude “for informal synthetic homotopy theory as done in this thesis, cubical ideas aren’t especially helpful in general”.

There is an important addendum to this picture however: I was recommended this paper in part because of its citation in a just released preprint, in which the results of this thesis (in slightly modified form) were fully mechanised in Cubical Agda by Axel Ljungström and Anders Mörtberg, allowing the ‘Brunerie number’ (that is, 2) to finally be computed from the proof that π4(S3)≅ℤ/nℤ for some integer n.

Discussing "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom"

(Link)

Authors: Cyril Cohen (INRIA Sophia Antipolis - Méditerranée), Thierry Coquand (University of Gothenburg), Simon Huber (University of Gothenburg), and Anders Mörtberg (Institute for Advanced Study)

Reference: Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), ed. Tarmo Uustalu, Leibniz International Proceedings in Informatics (LIPIcs), vol. 69 (2018).

Why this paper? Cited by Formalizing CCS and π-Calculus in Guarded Cubical Agda and Normalization and coherence for ∞-type theories

I’ve blogged a few times on homotopy type theory, ranging from the seminal book to various follow-ups (One Two Three). This is one of the most important follow-ups because of what it does to the univalence axiom, the cornerstone of homotopy type theory that asserts that equivalences between types correspond to identities between them. Cubical type theory is an instance of homotopy type theory for which the univalence axiom is not an axiom at all, but rather a provable theorem (inhabited type). The significance of this may not be immediately obvious to newcomers to type theory – who cares if a statement is an axiom or a consequence of some other rules? In fact with the type theories that lend themselves to applications such as interactive theorem proving we do not typically proceed by asserting axioms – unless we need to – but rather by defining rules for introducing and eliminating our basic type formers. Arranging things in this way allow us to have good computational properties, for example a constructive argument involving a natural number really will produce an appropriate natural number when run. This gives proofs in the type theory computational content, whereas the bald assertion of an axiom would provide a ‘roadblock’ in the execution of a proof.

This development proceeds by developing a type theory which has denotational semantics in the category of cubical sets. In this blog post I won’t sweat the details of these semantics – many of my comments last week about semantics in simplicial sets still apply  – although it is important to understand that working via the semantics motivates every part of this paper. However, I wish to concentrate on the details of the type theory itself as syntax.

It is fair to say that cubical type theory is a heavy duty extension to standard type theory. Some of the earlier parts of the paper are quite beautiful, however. The notion of identity as path is captured by thinking of them as (roughly) a function from a slightly abstracted version of the real interval [0,1] to a type; if we wish to express that t is equal u then we need that function to map 0 to t and 1 to u, and we’re done. This gives a startlingly simple proof of function extensionality (functions are equal if they agree on all inputs), which is a tricky property, and indeed sometimes not even true, in many type theories. Things get more involved, but still rather elegant, if we want dependence on multiple different arbitrary elements of the interval, usually called dimensions. This is where the cubes of cubical type theory come in, as zero dimensions give rise to a point in a space (which is to say, just a usual inhabitant of a type), and one dimension to a path in a space, but we can have squares, cubes, 4-dimensional hypercubes and so on as well.

The next feature is to define faces, which can be thought of as corresponding to faces of cubes (of various dimension), or more prosaically as restrictions on the values that our otherwise arbitrary interval elements can take. For example, we might require that both i and j are equal to one of 0 or 1, describing the outline of a square but leaving its centre unfilled. Terms and types defined with faces in their context are then only partial, e.g. only existing where the free dimensions i and j have appropriate values. Systems are terms of arbitrary type that explicitly define different constructions for different faces. Faces are also used to introduce the notion of extensibility;  a partial term t with respect to face φ is extensible if there is a term u that is not restricted to φ, for which if φ is added to its context, it is indeed equal to t. A new composition operator then comes into play that ensures that extensibility is preserved along paths. This may seem heavy, but is necessary to prove the rather mundane fact that identity is transitive. The equality judgements (intuitively, reduction rules) associated with the composition operator are fairly complex, depending on the type the composition is applied at and so needing explicit definition corresponding to each type former.

The final layer of novelty involves a new type former called glueing which connects types with partial types, and ensures that extensibility is invariant across equivalence. This is the final necessary ingredient for univalence (which is a statement about equivalences, after all) to be proved.

Discussing "The Simplicial Model of Univalent Foundations (after Voevodsky)"

(Link)

Authors: Krzysztof Kapulkin (University of Pittsburgh) and Peter LeFanu Lumsdaine (Institute for Advanced Study)

Reference: Krzysztof Kapulkin, Peter LeFanu Lumsdaine, The simplicial model of Univalent Foundations (after Voevodsky). J. Eur. Math. Soc. 23 (2021), no. 6, pp. 2071–2126. DOI 10.4171/JEMS/1050

Why this paper? Cited by Normalization and coherence for ∞-type theories, The Formal Theory of Monads, Univalently, and On the ∞-topos semantics of homotopy type theory

This paper has a rather peculiar publication history, as it started as a 2012 preprint written by the two authors along with a third, Fields medal winning mathematician Vladimir Voevodsky, who was in fact the main author. However Voevodsky grew disenchanted with the paper due to some issues with the type theory literature it was relying on, and asked for his name to be removed. Sadly, Voevodsky passed away before rectifying these holes in the literature, and so Kapulkin and Lumsdaine worked the paper into a publication. Lacking permission to re-add Voevodsky’s name to the author list, his contribution is instead recognised in the title.

One benefit of this paper having almost a decade to germinate is that it has a particularly pleasant and well written introduction to its topic, Homotopy Type Theory (HoTT). I looked at the seminal HoTT book on this blog last year; this paper picks up one of the topics that the book does not address, although it is briefly mentioned, namely denotational semantics. To recap, HoTT is an approach to mathematical foundations that aims to be both usable by humans and amenable to computer formalisation. The technical approach is to extend previous approaches to type theory with, in particular, a property called the univalence axiom (the other major innovation, higher inductive types, are not discussed here).  Univalence strengthens the usual notion of equality in type theory to, at the type level, correspond to equivalence; this means that one can move constructions and results between equivalent mathematical settings, a common feature of mathematical argument, ‘for free’. This leads one to think of types as (some sort of topological) space, with equality as paths in a space à la homotopy theory.

This paper makes this connection formal by giving homotopy type theory denotational semantics in the category of simplicial sets. Denotational semantics give a mathematical meaning for the constructions of a type theory, programming language, or logic. So long as the mathematical model chosen is not pathological, this gives us as immediate benefit a proof of consistency (one cannot prove false, or construct an element of a type that should be empty). Just as importantly, this style of semantics assures us that all syntactic constructions are not mere shuffling of symbols, but have real mathematical meaning that can be communicated to someone who is not necessarily interested in the details of the particular type theory. Put another way, the type theory is ‘about something’ other than itself.

Why is the ‘something’ that HoTT is about in this paper – i.e. simplicial sets – actually interesting, beyond mere proof of consistency? This paper does not offer an introduction to this mathematics, but looking at one of the books cited as background (link to pdf) gives some clues: “the category of simplicial sets has a homotopical structure … the resulting homotopy theory is equivalent in a strong sense to the ordinary homotopy theory of topological spaces… Insofar as simplicial sets are algebraically defined, and the corresponding closed model structure is combinatorial in nature, we obtain an algebraic, combinatorial model for standard homotopy theory”. In other words, simplicial sets are not a mere mathematical curiosity than happens to work for this type theory, but rather a strongly motivated approach to the general study of homotopy which, of course, is what motivated homotopy type theory in the first place. It should be noted that simplicial sets are not unique in having this property; there is a somewhat similar structure called cubical sets that appear to be more suited to computational implementation. But that, perhaps, is a story for another day.

Discussing "Internal Universes in Models of Homotopy Type Theory"

(Link)

Authors: Daniel R. Licata (Wesleyan University), Ian Orton (University of Cambridge), Andrew M. Pitts (University of Cambridge), and Bas Spitters (Aarhus University)

Reference: D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters. “Internal Universes in Models of Homotopy Type Theory”. In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Ed. by H. Kirchner. Vol. 108. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018, 22:1–22:17. doi: 10.4230/LIPIcs.FSCD.2018.22.

Why this paper? Cited by Homotopy type theory as internal languages of diagrams of ∞-logoses and mitten: a flexible multimodal proof assistant

Although this paper has among its authors my PhD supervisor (Andy) and a former collaborator (Bas), it did not give up its secrets easily, for me at least, thanks to the high technical level in the introduction alone. But, like an early Christmas present, I think there’ s something pretty interesting in here once it is unwrapped.

The story starts with homotopy type theory (on which I have written before), a proposal to improve the treatment of equality in the type-theoretic foundations of mathematics. It continues with cubical type theory, a first shot at actually implementing homotopy type theory. While homotopy type theory can be understood via a general notion of path-up-to-continuous-deformation in a space, cubical type theory is understood through a specific such space, namely the cubical sets. Never mind precisely what they are; it is enough for this less technical blog post to know that there is an interpretation of cubical type theory in some mathematical structure that allows one to give meaning to all constructions. One technicality that is important for understanding the paper of today is that the naïve approach to extracting a type theory from cubical sets (which can be done because the cubical sets form a topos) does not give quite the right thing. One needs the naïve notion of type to come equipped with something extra, called a composition structure; we call types with such structure fibrant. Not every cubical set is fibrant (else we would not have to explicitly require the structure). For example the interval cubical set which is used to define the notion of path, and hence equality, is not itself fibrant, so is not a first class type.

Today’s paper is part of an effort to define the correct notion of model of cubical type theory in type theory itself. This may seem quixotic but is in fact well motivated: such a definition is suitable for machine checking (and indeed this is done by formalising this paper in an Agda fork called Agda-flat), can be simpler than a more standard definition, and can also be more general, which raises the possibility of shifting from cubical sets to some other model if such a shift were found to be more appropriate for some purpose. However cubical sets are not abandoned altogether; the acid test for the type theory used in this paper is whether everything works in the ‘internal language’ of cubical sets (here again we use the fact that we have a topos, and any such comes equipped with its own native type theory).

The problem with the literature up until this paper is that attempts to formalise a model of cubical type theory in this style had not yet included any universe types. Universes are less cosmic than they sound (although the problems they throw up can be mind-expanding), but are rather a standard feature of dependent type theory that allows us to blur or even erase the distinction between types and terms; types are simply terms inside some universe type (more than one such type is required because otherwise we get the universe type as a member of itself, which throws up Russell-style paradoxes). Universes are an indispensable tool for such type theories, allowing one to use the useful constructions of the term-level language to define new types. The omission of universes from the earlier work was not an accident, but stems from an observation of Orton and Pitts that adding universes in the standard way in fact leads to a contradiction. This is related to a fact that not all families of fibrant types - which is to say, correct types for cubical type theory - are themselves fibrant; but if we want universes to be first class types, they must indeed be fibrant.

The solution to this is perhaps a bit surprising (although it is anticipated somewhat by earlier work by Michael Shulman), as it comes from modal logic, or more precisely, modal type theory. In particular there is a ‘global elements’ functor on cubical sets that behaves like the box modality of the intuitionistic version of a well known modal logic called S4. For this reason, techniques in type theory developed for that modal logic are applicable to that functor, namely a `dual zone’ variables context. Here all variables in one zone, called the ‘crisp’ variables, implicitly have the functor applied to them. Any term that is then substituted for a crisp variable must itself depend only on crisp variables. This notion is put to work in the definition of the ‘code’ and ‘elements’ constructions which relate types to elements of universes, as the dependencies in their definitions are required to be crisp, which precisely blocks the earlier proof of contradiction. A final argument which revolves around the interval having a property called ‘tininess’ shows that not only does the universe thus defined enjoy the properties it should have, but that it does so uniquely.

Discussing 'Homotopy Type Theory: Univalent Foundations of Mathematics'

 (Link)

Author: The Univalent Foundations Program (Institute for Advanced Study)

Why this paper? Cited by Internal Strict Propositions Using Point-Free Equations, Probabilistic Programming and Multiverse Models of Type Theory, and Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract).

The first thing to note about this e-book is its unusual authorship - it was put together by a collective of 27, along with various visitors and students, working together at the IAS in Princeton across a special year of study. The most famous participant was the Fields Medal (roughly equivalent to a Nobel Prize for mathematics) winner Vladimir Voevodsky, who sadly passed away a few years ago, aged just 51.

I will not attempt to summarise a 490 page book in a short blog post, but I can give some sense of the flavour of this work. It concerns a foundation of mathematics known as type theory. A foundation of mathematics might sound like an abstruse thing, and sometimes it can be, but it is essentially a description of what things mathematicians are able to talk about, and the rules they must follow to construct valid arguments about them. Nailing this down precisely is becoming increasingly vital, as we grow to understand that some mathematics (for example, proofs about software) can get too complex to fully trust a pen-and-paper proof by a human. The alternative is to have a somewhat simple-minded but indefatigable computer program check every step of a proof for error; for this to be possible, we must be precise about what language the program should be able to read and inferences it should be prepared to accept – in other words, our foundation of mathematics. Type theory is an approach to foundations that naturally lends itself to this sort of automated proof checking, as it involves working with syntax not too far from that of a programming language (although one of the arguments of this book is that one can de-formalise type theory to present proofs in a style more natural for human mathematicians as well).

This book introduces a new (at the time) direction in type theory known as homotopy type theory. The motivation is to get better behaviour for proofs of equality in type theory, with particular attention to applications in mathematical areas such as topology and category theory. The standard approaches to equality in type theory are well understood but rather blunt. The intensional approach only identifies functions (for example) when they have the same definition, up to some automatic simplifications a computer can easily run, and so will often not identify functions that produce the same output on all inputs, because their definitions differ – this is a reasonable approach to equality, but rather more limited than the use of equality in ordinary mathematics. The extensional approach, which ignores the details of definitions, lacks appealing computational properties. The insight that led to this book was that we can get a more nuanced notion of equality if we think of objects in our type theory as points in spaces, with equalities as paths between them modulo continuous deformation, a point of view taken from the mathematical field of homotopy theory. This concept takes some out of their mathematical comfort zone, but the idea has more to offer than better support for formalisation of homotopy theory itself (although it does offer that); borrowing the notion of path gives rise to a new notion of type theory in which equality has more interesting properties, and in particular does not collapse to mere definitional equality or something impossible to compute with.

The main new technical gains of taking the homotopy point of view into type theory are the univalence axiom, and higher inductive types. The univalence axiom essentially says that one can treat an equivalence (roughly, a mathematical proof that two objects are essentially ‘the same’), the same way one treats the type-theoretic construct of equality. Practically, this means that once one has proved an equivalence between two mathematical definitions, one can treat them as identical for all purposes, even switching back and forth during a proof to use whichever definition is most convenient at a given time, without risk of error. This mirrors standard informal mathematical practice but is sometimes considered an ‘abuse of notation’, i.e. something that should really be avoided in a fully rigorous development. With homotopy type theory, it is correct and completely formal to work like this. Higher inductive types are a general approach to constructing mathematical objects which include equalities as part of their inductive definition, and are vital for work formalising homotopy theory, but are also shown to be useful to other applications, for example to define the notion of colimit in category theory, and that of quotients of sets.