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.