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.