Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this is the “convenience factor” provided by univalence: it saves you from doing a lot of tedious proofs that constructions respect equality.  When restricted to sets, univalence says that all constructions respect bijection, and this can be used to build algebraic structures in such a way that isomorphic structures are equal (e.g. equality of groups is group isomorphism), and therefore all constructions on structures automatically respect isomorphism. When restricted to 1-types, univalence can be used to define categories in such a way that equivalent categories are equal, and therefore all constructions are non-evil; moreover, these non-evil categories can coexist with a notion of strict category, which can be used when finer distinctions are necessary.  In these applications, one defines the mathematical entities in question in a more or less traditional manner (a group is a type equipped with a multiplication operation, etc.), and univalence provides some theorems for free about constructions on these entities.

However, another reason we believe that HoTT will be a better framework, at least for certain kinds of math, is that it provides a direct way of working with something called ∞-groupoids.  ∞-groupoids are an infinite-dimensional generalization of the categorical notion of a groupoid (which is a category where every morphism is invertible).   Where a groupoid has just objects and morphisms, ∞-groupoids have objects, morphisms, morphisms between morphisms (2-morphisms), … all the way up.  ∞-groupoids are a complex structure: Morphisms at each level have identity, composition, and inverse operations, which are weak in the sense that they satisfy the groupoid laws (associativity of composition, identity is a unit for composition, inverses cancel) only up to the next level morphisms.  Because of weakness, it is quite difficult to describe all of the operations/properties of morphisms.  For example, because associativity of composition of morphisms (p o (q o r) = (p o q) o r) is itself a higher-dimensional morphism, one needs an additional operation relating different proofs of associativity; for example, the different ways to reassociate p o (q o (r o s)) into  ((p o q) o r) o s  give rise to Mac Lane’s pentagon.  Weakness also creates non-trivial interactions between levels, such as the middle-four interchange law.

Now, the really cool thing about using HoTT to work with ∞-groupoids is  that you don’t start by defining “an ∞-groupoid is…“ like one would in any other framework—which is fortunate, because describing the structure of an ∞-groupoid in something like set theory is notoriously difficult, because of all the structure mentioned above.  Instead, you exploit the fact that every type in type theory is an ∞-groupoid, with the structure of morphisms, 2-morphism, 3-morphisms, … given by the identity type (“propositional equality”).

Eventually, we hope to show that you can do a lot of math in an elegant way by working directly with ∞-groupoids, but for now, the area that we have developed the most is homotopy theory.  I started writing an update on our recent progress doing homotopy theory in type theory, and realized that we didn’t have a post on the blog explaining the basics.  So this post will tell the basic story: what is homotopy theory?  How do we do it in type theory?  And later I’ll post an update with what we’ve been up to recently.

Classical Homotopy Theory

Topology is the study of spaces up to continuous deformation.  Algebraic topology is the use of tools from abstract algebra, like group theory, to tell whether two spaces are the same.  As a first cut, we can say that two spaces are “the same” when there is an isomorphism between them (continuous maps back and forth that compose to the identity), though we will refine this later.  For example, one basic construction in algebraic topology is the fundamental group of a space: Given a space X and a point x0 in it, one can (almost—see below) make a group whose elements are loops at x0 (paths from x0 to x0), with the group operations given by the identity path (standing still), path concatenation, and path reversal.  Isomorphic spaces have the same fundamental group, so fundamental group can be used to tell two spaces apart: if  X and Y have different fundamental groups, they are not isomorphic.  Thus, the fundamental group is an algebraic invariant that provides global information about a space, which complements the local information provided by notions like continuity.  For example, the torus (donut) locally looks like the sphere, but has a global difference: it has a hole in it.  One way to see this is to observe that the fundamental group of the sphere is trivial, but the fundamental group of the torus is not.

To explain why this is so, we need to be a little more precise about what the fundamental group is.  Consider a space X with a path p from x to y.  Then there is an inverse path !p from y to x.  Concatenating p with !p (written !p o p) gives a path from x to x, which should be the same as the identity path (witnessing one of the inverse cancellation laws of a groupoid).  However, in topology, a path p in X is represented as a continuous map from the interval [0,1] into X, where p(0) = x and p(1) = y—think of the interval as “time” and p as giving the point on the path at each moment in time.  Under this definition, !p o p (which walks from x to y, and then back along the same route, as time goes from 0 to 1) is not literally the same as the identity path (which stays still at x at all times).  So loops don’t actually form a group!

The way to fix this is to consider the notion of homotopy between paths. Because !p o p walks out and back along the same route, you know that you can continuously shrink !p o p down to the identity path—it won’t, for example, get snagged around a hole in the space.  Formally, a homotopy between functions f, g : X -> Y is a continuous map h : [0,1] * X -> Y such that h(0,x) = f(x) and h(1,x) = g(x).  In the specific case of paths p and q, which, remember, are represented by maps [0,1] -> X, a homotopy is a continuous map h(t,x) : [0,1] x [0,1] -> X, such that h(0,x) = p(x) and h(1,x) = q(x).  That is, it’s the image in X of a square, which fills in the space between p and q.  Homotopy is an equivalence relation, and operations like concatenation, inverses, etc. respect it.  Moreover, the homotopy-equivalence-classes of loops in X at x0 (where two loops p and q are equated when there is a based homotopy between them, which is a homotopy h as above that additionally satisfies h(t,0) = h(t,1) = x0 for all t) do form a group: while !p o p is not equal to the identity, it is homotopic to it!  So, we can fix up the above definition of the fundamental group of a space by defining it to be the group of loops modulo homotopy.

Returning to the example, we can see that the sphere is different than the torus because the fundamental group of the sphere is trivial (the one-element group), but the fundamental group of the torus is not.  The intuition is that every loop on the sphere is homotopic to the identity, because its inside is filled in.  In contrast, a loop on the torus that goes around the donut’s hole is not homotopic to the identity, so there are non-trivial loops.

It turns out that the fundamental group, which is written π1(X,x0), is the first in a series of homotopy groups that provide additional information about a space.  Fix a point x0 in X, and consider the constant path id at x0.  Then the homotopies between id and itself form a group (when you quotient them by homotopy), which tells you something about the two-dimensional structure of the space.  Then π3(X,x0) is the group of homotopies between homotopies,  and so on.  One of the basic questions that algebraic topologists consider is calculating the homotopy groups of a space X, which means giving a group isomorphism between πk(X) and some more direct description of a group (e.g., by a multiplication table or presentation).  Somewhat surprisingly, this is a very difficult question, even for spaces as simple as the spheres.  Here is a chart that lists the low-dimensional homotopy groups of the low-dimensional spheres (0 is the trivial group, Z is the integers, Zk is the the finite group Z mod k):

There are some patterns, but there is no general formula, and many homotopy groups of spheres are currently unknown.  Homotopy groups are just one of the algebraic invariants that people study; some others are the homology groups and cohomology groups, which are sometimes easier to calculate.

An interesting fact is that, while we started off by trying to classify spaces up to isomorphism, most of these algebraic tools in fact classify spaces up to something called homotopy equivalence.  Two spaces X and Y are homotopy equivalent iff there are maps f : X -> Y and g : Y -> X such that there is a homotopy between f o g and the identity function (and similarly for g o f).  This gives you a little wiggle room to “correct” maps that don’t exactly compose to the identity, but only miss by space that can be filled in.  Isomorphic spaces are homotopy equivalent, but not nice versa: for example, the disk is not isomorphic to the point, but it is homotopy equivalent to it.  The vast majority of the constructions one considers  (homotopy groups, homology and cohomology groups, etc.) are homotopy-invariant, in the sense that they respect homotopy equivalence.  For example, two homotopy-equivalent spaces have the same fundamental groups, essentially because the fundamental group was defined to be paths modulo homotopy.  Thus, these invariants are really properties of the homotopy-equivalence-classes of spaces, which are called homotopy types.  If you’re interested in showing disequalities of spaces, this still has bearing on the original problem of classifying spaces up to isomorphism: if two spaces have different fundamental groups, then they are not homotopy equivalent, and therefore not isomorphic.  One reason the fact that all of these notions are homotopy-invariant is important is that it enables a big generalization of classical homotopy theory.

Homotopy Theory of ∞-groupoids

Topological spaces are an instance of the notion of ∞-groupoid described above: every topological space X has a fundamental ∞-groupoid whose k-morphisms are the k-dimensional paths in X.  The weakness of the ∞-groupoid (the fact that the groupoid laws hold only up to higher-dimensional morphisms) corresponds directly to the fact that paths only form a group up to homotopy, because the k+1-paths are the homotopies between the k-paths.

Moreover, the view of a space as an ∞-groupoid  preserves enough structure to do homotopy theory (calculate homotopy/homology/cohomology groups, etc).  Formally, the fundamental ∞-groupoid construction is adjoint to the geometric realization of an ∞-groupoid as a space, and this adjunction preserves homotopy theory (this is called the homotopy hypothesis/theorem, because whether it is a hypothesis or theorem depends on how you define ∞-groupoid).  For example, you can easily define the fundamental group of an ∞-groupoid, and if you calculate the fundamental group of the fundamental ∞-groupoid of a space, that will agree with the classical definition of fundamental group. For the type theorists in the crowd: ∞-groupoids are an interface that topological spaces implement, and one can do homotopy theory using only the operations in the interface.  The only problem is that this interface is fairly difficult to work with… 

Homotopy Theory in Type Theory

Which is where type theory comes in!  Type theory is a formal calculus of  ∞-groupoids. Because you can do homotopy theory through the abstraction of  ∞-groupoids, you can do homotopy theory in type theory.  One might call this synthetic homotopy theory, by analogy with synthetic geometry, which is geometry in the style of Euclid: you start from some basic constructions (a line connecting any two points) and axioms (all right angles are equal), and deduce consequences from them logically.  Here, the basic constructions/axioms are the operations on ∞-groupoids and maps between them (∞-functors), as presented by the identity type Id M N in dependent type theory.  We will often refer to features of type theory by topological-sounding names (for example, thinking of p : Id M N as a “path” from M to N, or even writing Path M N for the identity type), but it’s important to keep in mind that we can only talk about these things through the abstraction of an ∞-groupoid.  

There are few really nice advantages of doing synthetic homotopy theory in type theory.  First, you can use proof assistants like Agda and Coq to check your proofs.  Second, we’re starting to see examples where working in type theory is suggesting new ways of doing proofs.  Third, it seems likely that we will be able to interpret type theory in a wide variety of other categories that “look like” ∞-groupoids, and, if so, proving a result in type theory will show that it holds in these settings as well. It remains to be seen how much homotopy theory we can do synthetically, but there are already some positive indication, which I’ll discuss in a following post.  

For now, I’d like to review the basic ingredients of doing synthetic homotopy theory in type theory, with some links to reading material:

Higher inductive types. To do some homotopy theory, we need some basic spaces (the circle, the sphere, the torus) and constructions for making new spaces (suspensions, gluing on cells, …).  These are defined using higher inductive types, which are inductive types specified by both point and path constructors.  

For example, the circle is inductively generated by base:S1 and loop:Path base base—an inductive type with one point and one non-trivial loop.  This inductive type describes the free ∞-groupoid with one object and one 1-morphism.  The elimination rule for the circle, circle induction, expresses freeness: a map f : S1 -> X, from the circle into some type X is specified by giving a point and a loop in X (the image of the generators), and the general rules for the identity type ensure that f preserves the groupoid structure (e.g. it commutes with composition).

Higher inductive types are very general, and allow one to build spaces that are specified by a CW complex, using suspensions, pushouts, etc.  This gives a logical/synthetic view of these spaces, where they are constructed as the free ∞-groupoid on some generators, and can be reasoned about using induction.  

Homotopy groups.  Having defined some spaces, we’d like to start calculating some algebraic invariants of them.  The homotopy groups have an extremely natural definition in the setting of ∞-groupoids/type theory.  The fundamental group of X at x0 is (to a first approximation—see below) just the identity type Id{X} x0 x0, or the morphisms of the ∞-groupoid; π2(X,x0) is just the identity type Id{Id{X} x0 x0} refl refl, or the 2-morphisms, etc.  So, calculating a homotopy group is just giving a bijection between an identity type and some other type, and proving that this bijection preserves the group structure.  For example, calculating the fundamental group of the circle consists of giving a bijection between Id{S1} base base and Int that sends composition of paths to addition.

The reason this problem is interesting is that the (higher) inductive definition of a type X presents X as a free ∞-groupoid, and this presentation determines but does not explicitly describe the higher identity types of X.   The identity types are populated by both the generators (loop, for the circle), and all of the groupoid operations (identity, composition, inverses, …).  As the above table for spheres shows, in higher dimensions the ∞-groupoid operations create quite a complex structure.  Thus, the higher-inductive presentation of a space allows you to pose the question “what does the identity type of X really turn out to be?”, though it can take some significant math to answer it.  This is a higher-dimensional generalization of a familiar fact in type theory: even for ordinary inductive types like natural numbers or booleans, it takes a bit of work to prove that true is different than false—characterizing the identity type at bool is a theorem, not part of the definition.

The one detail that I glossed over above is that the (iterated) identity type really gives what is called the path space of a space, which is not just the set of k-dimensional path, but a whole space of them, with their higher homotopies.  To extract the set of paths-modulo-homotopy, we can use something called truncation.

N-types and truncations.  One of Voevodsky’s early observations was that it is possible to define a homotopy-theoretic notion called being an n-type in type theory.  He called these “types of h-level n”, and started counting at 0, but many of us now call them type levels or truncation levels and use the traditional homotopy-theoretic numbering, which starts at -2.  A -2-type (“contractible”) is equivalent to the unit type.  A -1-type (“hprop”) is proof-irrelevant—any two elements are propositionally equal.  A 0-type (“hset”) has uniqueness of identity proofs—any two propositional equalities between its elements are themselves equal.  A 1-type is like a groupoid: it can have non-trivial morphisms, but all 2-morphisms are trivial.  And so on.  Categorically, n-types correspond to n-groupoids.

The predicate “X is an n-type” is part of a modality, which means that there is a corresponding operation of n-truncation that takes a type A and makes the best approximation of A as an n-type.  n-truncation equates (“kills”) all morphisms of level higher than n in A.  Truncations can be constructed using higher inductive types (see here and here) and are quite important to doing homotopy theory in type theory, because many theorems characterize some “approximation” of a space, where the approximation is constructed by truncation.

For example, the fundamental group of a space is defined to be the 0-truncation of the space of loops at x0, which produces the hset of paths modulo homotopy, killing the higher homotopies of the loop space.

Univalence.  The univalence axiom plays an essential role in calculating homotopy groups (this is a formal claim: without univalence, type theory is compatible with an interpretation where all paths, including e.g. the loop on the circle, are the identity).  You can see this in action in the calculation of the the fundamental group of the circle: the map from Id{S1} base base to Z is defined by mapping a path on the circle to an isomorphism on Z, so that, for example, loop o !loop is sent to successor o predecessor, and then applying the isomorphism to 0. Univalence allows paths in the universe to have computational content, and this is used to extract information from paths in higher inductive types.

Homotopy-theoretic and type-theoretic methods.  One of the cool things we’ve found is that there are different ways of doing proofs in homotopy type theory.  Some proofs use techniques that are familiar from traditional homotopy theory, whereas others are more type-theoretic, and consist mainly of calculations with the ∞-groupoid structure.  For example, Mike Shulman’s original calculation of the the fundamental group of the circle is more homotopy-theoretic, while mine is more type-theoretic.  You can read more about the difference between the two in this paper.

Those are the basic tools.  In the next post, I’ll give an overview of the current status of homotopy theory in HoTT.