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 '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.