Univalent Foundations at IAS

December 3, 2012

As many of you may know, the Institute for Advanced Study is sponsoring a year-long program, called “Univalent Foundations for Mathematics” (UF), which is developing the theory and applications of Homotopy Type Theory (HTT).  The UF program is organized by Steve Awodey (CMU), Thierry Coquand (Chalmers), and Vladimir Voevodsky (IAS).  About two dozen people are in residence at the Institute to participate in the program, including Peter Aczel, Andrej Bauer, Peter Dybjer, Dan Licata, Per Martin-Löf, Peter Lumsdaine, Mike Shulman, and many others.  I have been shuttling back and forth between the Institute and Carnegie Mellon, and will continue to do so next semester.

The excitement surrounding the program is palpable.  We all have the sense that we are doing something important that will change the world.  A typical day consists of one or two lectures of one or two hours, with the rest of the day typically spent in smaller groups or individuals working at the blackboard.  There are many strands of work going on simultaneously, including fundamental type theory, developing proof assistants, and formulating a body of informal type theory.  As visitors come and go we have lectures on many topics related to HTT and UF, and there is constant discussion going on over lunch, tea, and dinner each day.  While there I work each day to the point of exhaustion, eager to pursue the many ideas that are floating around.

So, why is homotopy type theory so exciting?  For me, and I think for many of us, it is the most exciting development in type theory since its inception.  It brings together two seemingly disparate topics, algebraic topology and type theory, and provides a gorgeous framework in which to develop both mathematics and computer science.  Many people have asked me why it’s so important.  My best answer is that it’s too beautiful to be ignored, and such a beautiful concept bmust be good for something!  We’ll be at this for years, but it’s too soon to say yet where the best applications of HTT will arise.  But I am sure in my bones that it’s as important as type theory itself.

Homotopy type theory is based on two closely related concepts:

  1. Constructivity.  Proofs of propositions are mathematical objects classified by their types.
  2. Homotopy.  Paths between objects of a type are proofs of their interchangeability in all contexts.  Paths in a type form a type whose paths are homotopies (deformations of paths).

Homotopy type theory is organized so that maps and families respect homotopy, which, under the identification of paths with equality proofs, means that they respect equality.  The force of this organization arises from axioms that specify what are the paths within a type.   There are two major sources of non-trivial paths within a type, the univalence axiom, and higher inductive types.

The univalence axiom specifies that there is an equivalence between equivalences and equalities of the objects of a universe.  Unravelling a bit, this means that for any two types inhabiting a universe, evidence for their equivalence (a pair of maps that are inverse up to higher homotopy, called weak equivalence) is evidence for their equality.  Put another way, weak equivalences are paths in the universe.  So, for example, a bijection between two elements of the universe \textsf{Set} of sets constitutes a proof of the equality (universal interchangeability) of the two sets.

Higher inductive types allow one to define types by specifying their elements, any paths between their elements, any paths between those paths, and so on to any level, or dimension.  For example, the interval, I, has as elements the endpoints 0, 1 : I, and a path \textsf{seg} between 0 and 1 within I.  The circle, S^1 has an element \textsf{base} and a path \textsf{loop} from \textsf{base} to itself within S^1.

Respect for homotopy means that, for example, a family F of types indexed by the type \textsf{Set} must be such that if A and B are isomorphic sets, then there must be an equivalence between the types F(A) and F(B) allowing us to transport objects from one “fiber” to the other.  And any function with domain \textsf{Set} must respect bijection—it could be the cardinality function, for example, but it cannot be a function that would distinguish \{\,0,1\,\} from \{\,\textsf{true},\textsf{false}\,\}.

Univalence allows us to formalize the informal convention of identifying things “up to isomorphism”.  In the presence of univalence equivalence types (spaces) are, in fact, equal.  So rather than rely on convention, we have a formal account of such identifications.

Higher inductives generalize ordinary inductive definitions to higher dimensions.  This means that we can now define maps (computable functions!) between, say, the 4-dimensional sphere and the 3-dimensional sphere, or between the interval and the torus.  HTT makes absolutely clear what this even means, thanks to higher inductive types.  For example, a map out of S^1 is given by two pieces of data:

  1. What to do with the base point.  It must be mapped to a point in the target space.
  2. What to do with the loop.  It must be mapped to a loop in the target space based at the target point.

A map out of I is given similarly by specifying

  1. What to do with the endpoints.  These must be specified points in the target space.
  2. What to do with the segment.  It must be a path between the specified points in the target space.

It’s all just good old functional programming!  Or, rather, it would be, if we were to have a good computational semantics for HTT, a topic of intense interest at the IAS this year.  It’s all sort-of-obvious, yet also sort-of-non-obvious, for reasons that are difficult to explain briefly.  (If I could, they would probably be considered obvious, and not in need of much explanation!)

A game-changing aspect of all of this is that HTT provides a very nice foundation for mathematics in which types (\infty-groupoids) play a fundamental role as classifying all mathematical objects, including proofs of propositions, which are just types.  Types may be classified according to the structure of their paths—and hence propositions may be classified according to the structure of their proofs.  For example, any two proofs of equivalence of two natural numbers are themselves equivalent; there’s only one way to say that 2+2=4, for example.  Of course there is no path between 2+2 and 5.  And these two situations exhaust the possibilities: any two paths between natural numbers are equal (but there may not even be one).  This unicity of paths property lifts to function spaces by extensionality, paths between functions being just paths between the range elements for each choice of domain element.  But the universe of Sets is not like this: there are many paths between sets (one for each bijection), and these are by no means equivalent.  However, there is at most one way to show that two bijections between sets are equivalent, so the structure “peters out” after dimension 2.

The idea to apply this kind of analysis to proofs of propositions is a distinctive feature of HTT, arising from the combination of constructivity, which gives proofs status as mathematical objects, and homotopy, which provides a powerful theory of the equivalence of proofs.  Conventional mathematics ignores proofs as objects of study, and is thus able to express certain ideas only indirectly.  HTT brings out the latent structure of proofs, and provides an elegant framework for expressing these concepts directly.

Update: edited clumsy prose and added concluding paragraph.

Higher-Dimensional Type Theory

May 30, 2011

Ideas have their time, and it’s not for us to choose when they arrive.  But when they do, they almost always occur to many people at more or less the same time, often in a slightly disguised form whose underlying unity becomes apparent only later.  This is perhaps not too surprising, the same seeds taking root in many a fertile mind.  A bit harder to explain, though, is the moment in time when an idea comes to fruition.  Often all of the ingredients are available, and yet no one thinks to put two-and-two together and draw what seems, in retrospect, to be the obvious inference.  Until, suddenly, everyone does.  Why didn’t we think of that ages ago?  Nothing was stopping us, we just didn’t notice the opportunity!

The recent development of higher-dimensional structure in type theory seems to be a good example.  All of the ingredients have been present since the 1970’s, yet as far as I know no one, until quite recently, no one quite put together all the pieces to expose the beautiful structure that has been sitting there all along.  Like many good ideas, one can see clearly that the ideas were foreshadowed by many earlier developments whose implications are only now becoming understood.  My plan is to explain higher type theory (HTT) to the well-informed non-expert, building on ideas developed by various researchers, including Thorsten Altenkirch, Steve Awodey, Richard Garner, Martin Hofmann, Dan Licata, Peter Lumsdaine, Per Martin-Löf, Mike Shulman, Thomas Streicher, Vladimir Voevodsky, and Michael Warren.  It will be useful in the sequel to be familiar with The Holy Trinity, at least superficially, and preferably well enough to be able to move back and forth between the three manifestations that I’ve previously outlined.

One-dimensional dependent type theory is defined by derivation rules for these four fundamental forms of judgement (and, usually, some others that we suppress here for the sake of concision):

\displaystyle \Gamma\vdash A\,\mathsf{type}

\displaystyle \Gamma\vdash M : A

\displaystyle \Gamma\vdash M \equiv N : A

\displaystyle \Gamma\vdash A\equiv B

A context, \Gamma, consists of a sequence of declarations of variables of the form x_1:A_1,\dots,x_n:A_n, where it is presupposed, for each 1\leq i\leq n, that x_1:A_1,\dots,x_{i-1}:A_{i-1}\vdash A_i\,\mathsf{type} is derivable.

The key notion of dependent type theory is that of a family of types indexed by (zero or more) variables ranging over a type.  The judgement \Gamma\vdash A\,\mathsf{type} states that A is a family of types indexed by the variables given by \Gamma.  For example, we may have \vdash\textit{Nat}\,\textsf{type}, specifying that \textit{Nat} is a closed type (a degenerate family of types), and x{:}\textit{Nat}\vdash\textit{Seq}(x)\,\textsf{type}, specifying that \textit{Seq}(n) is a type (say, of sequences of naturals of length n) for each \vdash n:\textit{Nat}.  The rules of type theory ensure, either directly or indirectly, that the structural properties of the hypothetical/general judgement are valid.  In particular families of types respect equality of indices:

\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad \Gamma\vdash M\equiv N:A \quad \Gamma\vdash P:B[M/x]}\over  {\Gamma\vdash P:B[N/x]}}.

In words, if B is a family of types indexed by A, and if M and N are equal members of type A, then every member of B[M/x] is also a member of B[N/x].

The generalization to two- (and higher-) dimensional type theory can be motivated in several ways.  One natural source of higher-dimensional structure is a universe, a type whose elements correspond to types.  For example, we may have a universe of sets given as follows:

\displaystyle \vdash \textit{Set}\,\textsf{type}

\displaystyle x:\textit{Set}\vdash \textit{Elt}(x)\,\textsf{type}

\displaystyle \vdash \textit{nat}:\textit{Set}

\displaystyle \vdash \textit{Elt}(\textit{nat})\equiv\textit{Nat}

\displaystyle a:\textit{Set},b:\textit{Set}\vdash a\times b : \textit{Set}

\displaystyle a:\textit{Set},b:\textit{Set}\vdash \textit{Elt}(a\times b)\equiv \textit{Elt}(a)\times\textit{Elt}(b)

and so forth, ensuring that \textit{Set} is closed under typical set-forming operations whose interpretations are given by \textit{Elt} in terms of standard type-theoretic concepts.

In many situations, including much of informal (yet entirely rigorous) mathematics, it is convenient to identify sets that are isomorphic, so that, for example, the sets \textit{nat}\times\textit{nat} and \textit{2}\to\textit{nat} would be interchangeable.  In particular, these sets should have the “same” (type of) elements.  But obviously these two sets do not have the same elements (one consists of pairs, the other of functions, under the natural interpretation of the sets as types), so we cannot hope to treat \textit{Elt}(\textit{nat}\times\textit{nat}) and \textit{Elt}(\textit{2}\to\textit{nat}) as equal, though we may wish to regard them as equivalent in some sense.  Moreover, since two sets can be isomorphic in different ways, isomorphism must be considered a structure on sets, rather than a property of sets.  For example, \textit{2} is isomorphic to itself in two different ways, by the identity and by negation (swapping).  Thus, equivalence of the elements of two isomorphic sets must take account of the isomorphism itself, and hence must have computational significance.

It is precisely the desire to accommodate equivalences such as this that gives rise to higher dimensions in type theory.  Specifically, we introduce two-dimensional structure by adding a new judgement to type theory stating that two members of a type are related by a specified transformation:

\displaystyle \Gamma\vdash \alpha :: M\simeq N : A

Crucially, families of types must respect transformation:

\displaystyle{{\Gamma,x:A\vdash B\,\textsf{type}\quad \Gamma\vdash \alpha :: M\simeq N:A \quad \Gamma\vdash P:B[M/x]}\over  {\Gamma\vdash \textit{map}\{x:A.B\}[\alpha](P):B[N/x]}}.

A transformation should be thought of as evidence of interchangeability of the members of a type; the map operation puts the evidence to work.

Returning to our example of the universe of sets, let us specify that a transformation from one set to another is an pair of functions constituting a bijection between the elements of the two sets:

\displaystyle{  {\begin{array}{c}  \Gamma,x:\textit{Elt}(a)\vdash f(x):\textit{Elt}(b) \\  \Gamma,x:\textit{Elt}(b)\vdash g(x):\textit{Elt}(a) \\  \Gamma,x:\textit{Elt}(a)\vdash g(f(x))\equiv x:\textit{Elt}(a) \\  \Gamma,x:\textit{Elt}(b)\vdash f(g(x))\equiv x:\textit{Elt}(b)  \end{array}}  \over  {\Gamma\vdash\textit{iso}(f,g)::a\simeq b:\textit{Set}}}

(The equational conditions here are rather strong; I will return to this point in a future post.  For now, let us just take this as the defining criterion of isomorphism between two sets.)

Evidence for the isomorphism of two sets induces a transformation on types given by the following equation:

\displaystyle{  {\Gamma\vdash M:\textit{Elt}(a)}\over  {\Gamma\vdash \textit{map}\{\textit{Elt}\}[\textit{iso}(f,g)](M)\equiv f(M) : \textit{Elt}(b)}}

(suppressing the obvious typing premises for f and g).  In words an isomorphism between sets a and b induces a transformation between their elements given by the isomorphism itself.

This, then, is the basic structure of two-dimensional type theory, but there is much more to say!  In future posts I intend to develop the ideas further, including a discussion of these topics:

  1. The definition of \textit{map}\{x:A.B\} is given by induction over the structure of x:A.B.  The above equation covers only one case; there are more, corresponding to each way of forming a family of types x:A.B.  The extension to function types will expose the role of the inverse of the isomorphism between sets.
  2. The judgement \alpha::M\simeq N:A may be internalized as a type, which will turn out to correspond to the identity type in Martin-Löf’s type theory, albeit with a different interpretation given by Altenkirch.  The identity type plays an important role in the extension to all higher dimensions.
  3. To ensure coherence and to allow for greater expressiveness we must also discuss equality and equivalence of transformations and how these influence the induced transformation of families of types.  In particular transformations admit a groupoid structure which expresses reflexivity, symmetry, and transitivity of transformation; these conditions can be considered to hold strongly or weakly, giving rise to different applications and interpretations.
  4. Higher-dimensional type theory admits a fascinating interpretation in terms of homotopy theory which types are interpreted as spaces, members as points in those spaces, and transformations as paths, or homotopies.  This, together with a generalization of the treatment of universes outlined above, is the basis for Voevodsky’s work on univalent foundations of mathematics.
  5. One may consider relaxing the groupoid structure on transformations to a “monoidoid” (that is, category) structure by not requiring symmetry (inverses).  The structure of type theory changes significantly in the absence of symmetry, posing significant open problems, but admitting a wider range of applications of higher-dimensional structure in both CS and mathematics.
To keep up to date with the latest developments in this area, please visit the Homotopy Type Theory blog!


Get every new post delivered to your Inbox.

Join 213 other followers