Homotopy Theory in Type Theory: Progress Report

Posted on 20 May 2013 by Dan Licata

A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic tools used in our synthetic approach to the subject (such as univalence and higher inductive types). The big open questions are: How much homotopy theory can one do in this synthetic style? And, how hard is it to work in this style, and to give computer-checked proofs of these results?

Thus far, our results have been quite encouraging on both of these fronts: We’ve done a significant swath of basic homotopy theory synthetically, including calculations of π_n(Sⁿ), π₃(S²), and π₄(S³); proofs of the Freudenthal suspension theorem, the Blakers-Massey theorem, and van Kampen’s theorem; a construction of Eilenberg-Mac Lane spaces; and a development of the theory of covering spaces. We’ve given computer-checked proofs for almost all of these results, and the process has been quite pleasant and fun. Lengthwise, the computer-checked proofs are comparable with, and in some cases shorter than, the same proof written out in a traditional style. Moreover, the proofs have involved a blend of classical homotopy theoretic ideas and type theoretic ideas. While most of what we have done is to give new proofs of existing results, these techniques have started to lead to new results, such as a proof of the Blakers-Massey theorem in general ∞-topoi (which we gave by translating the type-theoretic proof). Additionally, we have one example (π₄(S³)) illustrating the promise of the constructive aspects of homotopy type theory. Finally, these proofs have furthered our understanding of the computational aspects of homotopy type theory, particularly about computing with higher identity types.

This post will describe the results that we’ve gotten so far—particularly this spring, during the special year at IAS. This was a big collaborative effort: many people contributed to it, by being the principal author of a proof or formalization, by suggesting problems to work on, by giving feedback on results, or by contributing to discussions and seminars. When the spring IAS term started on January 14th, we had a proof that π₁(S¹) is Z and that π_k(S¹) is trivial otherwise (by Mike Shulman), and a proof that π_k(Sⁿ) is trivial for k<n (by Guillaume Brunerie). Here’s what that looks like in the chart of homotopy groups of spheres:

And, here’s what we had proved about homotopy groups of spheres by the end of the term (we’ll explain the grey/white highlights below):

Let’s go through the theorems that fill in this table:

In the first row, S⁰ is the booleans, so these calculations follow from Hedberg’s theorem, which entails that the booleans are a set.
In the second row, S¹ is the circle. Our calculation of this row consists of showing that the loop space of the circle (Ω(S¹)) is Z: Applying truncation to both sides shows that π₁(S¹) is Z. Moreover, because the higher homotopy groups of a type are constructed from the loop space of that type, we get that that the higher homotopy groups of the circle are the same as the higher homotopy groups of Z, and therefore trivial, again because Z is a set.
We have a few different proofs that Ω(S¹) is Z. The first (by Mike Shulman), follows a standard homotopy-theoretic argument, showing that the total space of the universal cover of the circle is contractible. Another (by Guillaume Brunerie) shortens the original proof significantly, by factoring some of the reasoning out into a flattening lemma about total spaces of fibrations defined by recursion on higher inductives. Another proof (by Dan Licata) avoids calculating the total space of the cover, instead relying on calculations using the definition of the cover by circle recursion. The template introduced in this proof is now known as the encode-decode method.
The all-0 diagonals (the colored diagonals below the π_n(Sⁿ) diagonal) state that π_k(Sⁿ) is trivial for k<n. We have a few different proofs of this now. In fact, we have two definitions of the n-sphere (which should coincide, but we haven’t proved this yet). The first is by induction on n: S¹ is the circle, and the (n+1)-sphere is the suspension of the n-sphere. The second uses a fancy form of higher inductive types: First, we define the n-fold iterated loop space of a type, Ωⁿ(A), by induction on n. Then, we define the n-sphere to be a higher inductive type with one point and one element of Ωⁿ. The circle is generated by a point and a single 1-dimensional loop; the 2-sphere by a single point and a single 2-dimensional loop, and so on. This form of higher-inductive type is a bit unusual (and has not been formally studied): for each instantiation of n, the n-loop constructor is an element of a path type of Sⁿ, but the level of iteration of the path type depends on n, and when n is a variable, Ωⁿ is not syntactically a path type. However, the fact that the homotopy groups have come out right so far provides some indication that this is a sensible notion.
The first proof of π_k<n(Sⁿ) (by Guillaume Brunerie), for the suspension definition of the spheres, uses a connectedness argument. The second (by Dan Licata), for the iterated-loop-space definition, uses the encode-decode method. A third (by Dan Licata) uses a connectedness argument for π₁ and then uses the Freudenthal suspension theorem (see below) to induct up.
For a long time after the first proof of π₁(S¹) in spring 2011, we were stuck on calculating any non-trivial higher homotopy groups. The thing that really broke the dam open on these was a proof of π₂(S²) (by Guillaume Brunerie), which goes by way of proving that the total space of the Hopf fibration (as constructed by Peter Lumsdaine) is S³. This gives π₂(S²), and also implies that π_k(S²) = π_k(S³), for k>=3. Because we have now calculated π₃(S³) (see below), this gives π₃(S²) = Z. Because we have now calculated most of π₄(S³) (see below; the “most of” disclaimer is why these squares are shaded white in the table), this gives most of π₄(S²). The grey shading on the remainder of the S²/S³ rows indicates that while we have not calculated any of these groups, we know that the two rows are equal.
The calculation of the total space of the Hopf fibration has proved difficult to formalize, because a key lemma requires some significant path algebra. However, only a couple of days after the first proof of π₂(S²), we had a computer-checked one (by Dan Licata), using the encode-decode method, with the Hopf fibration playing the same role that the universal cover plays for S¹. This proof bypasses showing that the total space of the Hopf fibration is S³, so it doesn’t give all the nice corollaries mentioned above. But it also illustrates that type theory can lead to shorter and more “beta-reduced” proofs of these theorems. This proof was for the iterated-loop-space definition of S², but we eventually developed an encode-decode proof (also by Dan Licata) for the suspension definition.
Next, we have the π_n(Sⁿ) = Z diagonal. The proof is by induction on n, using π₁(S¹) in the base case, and proving that π_n(Sⁿ) = π_n+1(Sⁿ⁺¹) in the inductive step. We have a couple of proofs of this. The first (by Dan Licata and Guillaume Brunerie) is a generalization of the encode-decode proof of π₂(S²). It took about two weeks to develop and formalize the proof, much of which is a library exploring the type theory of iterated loop spaces. The second proof, for the suspension definition of the spheres, uses the Freudenthal suspension theorem.
The Freudenthal suspension theorem gives the connectedness of the path constructor for suspensions. It implies that all entries in the colored diagonals in the above chart are the same. Therefore, it suffices to compute one entry in each diagonal. We have done this for π_k<n(Sⁿ), for π_n(Sⁿ), and for π_n+1(Sⁿ) (shaded white). The remaining diagonals are shaded grey because we have proved that all entries are the same, but we haven’t calculated any individual entry.
The proof of the Freudenthal suspension theorem (by Peter Lumsdaine; formalized by Dan Licata) is an interesting combination of the encode-decode method used in π_n(Sⁿ) with the homotopy-theoretic notion of connectedness of maps and spaces. Indeed, the tower of results going from π₂(S²) to π_n(Sⁿ) to Freudenthal really illustrates the promise of the interaction between homotopy theory and type theory: we started with a more homotopy-theoretic proof of π₂(S²), which led to a more type-theoretic proof of π₂(S²) (using the encode-decode method), which led to a more type-theoretic proof of π_n(Sⁿ), which led to a proof of the Freudenthal suspension theorem that combines these type-theoretic aspects with some additional homotopy-theoretic ideas about connectedness.
In the π_n+1(Sⁿ) = Z₂ diagonal, we have a proof (by Guillaume Brunerie) that there exists a k such that π₄(S³) = Z_k, using the James construction. This diagonal is shaded white because this isn’t quite the classical result: we should also check that k is 2. However, this proof illustrates the promise of a computational interpretation of homotopy type theory: the proof is constructive, so to check that k is indeed 2, all we would need to do is run the program!

In addition to homotopy groups of spheres, we have proved the following theorems:

The Freudenthal suspension theorem gives information about spaces other than spheres. For example, we have a construction (by Dan Licata) of Eilenberg-Mac Lane spaces K(G,n), which are a basic building block that can be used to construct spaces up to homotopy equivalence. For an abelian group G, K(G,n) is a space whose nth homotopy group is G, and whose other homotopy groups are trivial; for example, K(Z,n) is equivalent to the n-truncation of the n-sphere. We first construct K(G,1), and then construct K(G,n) by suspending K(G,1) and truncating. The proof that it has the right homotopy groups uses the Freudenthal suspension theorem, generalizing the proof from Freudenthal that π_n(Sⁿ) = Z.
The Freudenthal suspension theorem gives the connectivity of the path constructor of a suspension. A generalization of suspensions is the notion of a pushout, and the generalization of Freudenthal to pushouts is the Blakers-Massey theorem. We have a proof of Blakers-Massey (by Peter Lumsdaine, Eric Finster, and Dan Licata; formalized by Favonia). We have also translated this proof to the language of ∞-topoi, which proves the result in a more general setting than was previously known.
van Kampen’s theorem characterizes the fundamental group of a pushout. We have a proof (by Mike Shulman; formalized by Favonia) using the encode-decode method.
To calculate π₁(S¹), we used the universal cover of the circle. This is an instance of a general notion of covering spaces, and the fact that covering spaces of a space correspond to actions by its fundamental group. Favonia formulated and formalized the theory of covering spaces.

You can find out more about these results in the following places:

Many of these results are written up in an informal style in the forthcoming book Homotopy Type Theory: Univalent Foundations of Mathematics
There are many videos of talks on these results:
- A good place to start is this end-of-the-term lecture summarizing the results.
- A Computer-Checked Proof that pi_1(S^1) is Z
- The Hopf Fibration via Higher Inductive Types
- pi_2(S^2) in HoTT
- The James Construction and pi_4(S^3)
- Eilenberg-Mac Lane Spaces in HoTT
- Cohomology in Homotopy Type Theory
- Formal Abstract Homotopy Theory
- Toward Higher Inductive Types
- Semantics of Higher Inductive Types
Some individual results/tools have been written up:
- For π₁(S¹), see these blog posts, and this paper.
- Covering spaces
- Higher inductive types
- How to fake higher inductive types in current proof assistants
- Truncations
All of the computer-checked proofs are available online; see here and here and here. This wiki page has pointers to specific results.

Finally, there is a lot of low-hanging fruit left to pick! If you are interested in getting involved, leave a comment, or send an email to someone mentioned above (or to the HomotopyTypeTheory google group).

Posted in Higher Inductive Types, Homotopy Theory | 6 Comments

Universe n is not an n-Type

Posted on 15 May 2013 by Nicolai Kraus

Joint work with Christian Sattler

Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here.

One of the most basic consequences of the univalence axiom is that the universe of types is not a set, i.e. does not have unique identity proofs. It is plausible to expect that the next universe $U_1$ is not a groupoid, i.e. its path-spaces are not sets, but a proof of that is already surprinsingly difficult.

We prove the generalized statement, namely that $U_n$ is not an n-type. At the same time, our construction yields, for a given $n$ , a type that is an $(n+1)$ -type but not an n-type. This answers one of the questions asked at the UF Program. The proof works in basic MLTT with $\Sigma$ -, $\Pi$ - and identity types as well as a sequence of universes. We need the uivalence axiom, but no other “HoTT-features”.

We also have a pdf version of the proof.

Posted in Code, Foundations, Talk, Univalence | Leave a comment

Covering Spaces

Posted on 27 April 2013 by favonia

Covering spaces are one of the important topics in classical homotopy theory, and this post summarizes what we have done in HoTT. We have formulated the covering spaces and (re)proved the classification theorem based on (right) $\pi_1(X)$ -sets, i.e., sets equipped with (right) group actions of the fundamental group $\pi_1(X)$ . I will explain the definition and why we need some constancy factorization trick in the proof.

Definition

So, what are covering spaces in HoTT? The core ingredient of covering spaces is a fibration, which is easy in HoTT, because every function or dependent type in HoTT can be viewed as a fibration (up to homotopy). The only problem is the possible higher structures accidentally packed into the space (which are usually handled separately in classical homotopy theory). To address this, we have another condition that each fiber is a set. These two conditions together match the classical definition. More precisely, given a base space $X$ , a covering is a mapping $f$ from $X$ to some universe (or, a type family indexed by $X$ ) where for each $x \in X$ we know $f(x)$ is a set.

One can also formulate coverings as mappings instead of type families. I personally prefer the latter because they seem easier to work with in type theory. Note that we did not assert that the base space $X$ is path-connected or pointed, which are required by interesting theorems (ex: the classification theorem) but not by the definition.

Classification Theorem

The classification theorem says there is an isomorphism between $\pi(X,x_0)$ -set and covering spaces. Here we assume $X$ is path-connected and pointed (based) at $x_0 \in X$ .

The direction from covering spaces to $\pi(X,x_0)$ -sets is easier, since the set can simply be the fiber over the point $x_0$ , and the group action can be defined as transporting along an element in the homotopy group. The other direction is more challenging, requiring an explicit construction of the covering space from the given $\pi(X,x_0)$ -set. Naturally, the fiber over $x_0$ should be the underlying set, but what about other fibers? For arbitrary point $x$ in $X$ , due to the connectedness of the base space $X$ , there exists a (truncated) path from $x_0$ to $x$ , which can be used to transport everything in the fiber over $x_0$ to the fiber over $x$ . However, unless the homotopy group is trivial, one needs to identify multiple copies produced by different paths. We simply threw in gluing 1-cells and then made each fiber a set.

The above higher inductive type, which is called ribbon in the library, goes as follows: It is parametrized by the $\pi(X,x_0)$ -set, the underlying set $Y$ , the group action $\bullet$ , and the point $x$ in focus. The trace constructor “copies” everything from the fiber over $x_0$ to the fiber over $x$ along some path in the base type, and the paste constructor glues multiple copies made by different paths.

data ribbon (Y : Set) (∙ : Action Y) (x : X) : Set where
  trace : Y → Truncated 0 (x₀ = x) → ribbon x
  paste : (y : Y) → (loop : Truncated 0 (x₀ = x₀))
        → (p : Truncated 0 (x₀ = x))
        → trace (y ∙ loop) p ≡ trace y (loop ∘ p)

The most interesting part is to show that creating ribbons is left inverse to constructing $G$ -sets as mentioned in the beginning of the section. It suffices to show that ribbons indeed form the original covering space, which is, by functional extensionality, equivalent to demonstrating that they are fiberwise equivalent. The trouble is that, for a point $x \in X$ and a point $y$ in the fiber of the input covering over $x$ , one needs a path $x_0 = x$ to even make one point in the ribbon; while we can get a $(-1)$ -truncated path out of the connectedness condition, the constructor requires a $0$ -truncated path.

The constancy comes to rescue! It can be shown that, if there is a function $f$ from $A$ to a set $B$ , and $f$ is constant, then $f$ factors through $|A|$ with ideal computational behaviors. In our case, different points generated by different paths will be glued together by the paste constructor and moreover each fiber is a set. Therefore we can apply this lemma to establish the fiberwise equivalence, and hence the theorem!

Remarks

We also proved that the homotopy group itself corresponds to the universal covering, where universality is defined as being simply-connected. The ribbon construction, as an explicit description for covering spaces, comes in handy. In addition, we calculated $\pi(S^1)$ (again) with the new library; however, even with aggressive Agda optimization, the complexity remains—one still needs to prove the contractibility of some covering of $S^1$ for universality. Perhaps there are other better examples which can show the real power of this isomorphism?

The Agda code is currently available at http://hott.github.io/HoTT-Agda/Homotopy.Cover.HomotopyGroupSetIsomorphism.html but we are rebuilding the whole library. This link might not be valid after the migration.

Posted in Code, Higher Inductive Types, Homotopy Theory | 5 Comments

Homotopy Theory in Homotopy Type Theory: Introduction

Posted on 8 March 2013 by Dan Licata

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.

Posted in Applications, Higher Inductive Types, Homotopy Theory, Uncategorized, Univalence | Leave a comment

Running Spheres in Agda, Part II

Posted on 11 February 2013 by favonia

(Sorry for the long delay after the Part I of this post.)

This post will summarize my work on defining spheres in arbitrary finite dimensions (Sⁿ) in Agda. I am going to use the tools for higher-order paths (discussed in Part I) to build up everything for spheres. There are many ways to define a sphere and I will stick with the “one 0-cell and one n-cell” definition in this post. One important feature is that I have achieved full compatibility with previous ad-hoc definitions for specific dimensions (ex: S²) except for one small caveat mentioned below. That is, this is a drop-in replacement for spheres ever defined for any fixed dimension in 95% cases. The code is available at this place.

Why is this Difficult?

The most difficult thing is the computation rule for loops. It is tricky to get the types right, and is even trickier to derive the non-dependent rule from the dependent one. Intuitively, this rule says “if I plugged in some data for the loop in the eliminator, then applying this instantiated eliminator to the original loop will recover that data I plugged in”. This looks fine, except that the types do not (immediately) match in Agda. We need to find a way to talk about the types of the plugged-in data without mentioning the eliminator itself. The reason is that, when we are declaring the eliminator, the type cannot mention the name of the eliminator itself in Agda (at least in my understanding). However, when you are applying this instantiated eliminator to the original loop, the result will have the eliminator in the type, and in general it is not definitonally equal to the type we used in the declaration of the eliminator. This mismatch becomes a serious problem for arbitrary finite dimensions.

S¹ in Agda luckily avoids this problem because of the definitional equality for 0-cells (base points) and its finite dimension. However, it can still illustrate the problem if we pretend that there was only evidential equality for 0-cells. Let’s look at the type of eliminator in Agda:

S¹-elim : ∀ {ℓ} (P : S¹ → Set ℓ) (pbase : P base)
          → subst P loop¹ pbase ≡ pbase
          → (x : S¹) → P x

pbase is the data for the base point and subst P loop¹ pbase ≡ pbase is the type of the data for the loop. The holy grail of the definition of S¹ is then the following equivalence:

cong[dep] P (S¹-elim P pbase ploop) loop¹ ≡ ploop

where cong[dep] is the dependent map on paths (which is named map or apd in different HoTT libraries). This equivalence means that we can recover the plugged-in data by applying the eliminator to the original loop. The trouble is that this is ill-typed unless we have some definitional equality. The type of the left-hand side is actually

subst P loop¹ ((S¹-elim pbase ploop) base) ≡ ((S¹-elim pbase ploop) base)

while the right-hand side is of type

subst P loop¹ pbase ≡ pbase

How do we know that the eliminator applied to the base point is indeed the data for the base point? This is why the Coq library required (thanks to a recent patch) ~~requires (or at least “required”—I am not aware of the possible recent development)~~ some extra work to bridge the gap in types. When we are defining spheres for a particular dimension, the type checker (equivalently) kindly expands the expressions down to eliminators applied to the base points. (This is of course not what a type checker in Coq/Agda really does.) The way we use Agda will establish the definitional equivalence between this application and the data for the base point, and so the type checker is satisfied.

Nonetheless, Agda cannot expand the expressions for us if we are talking about spheres in arbitrary finite dimensions. It requires an induction on the dimension to show that two things are equivalent, which is beyond the ability of the current type checker. We need to prove the equivalence by ourselves.

In the following paragraphs I will describe how I have proved necessary lemmas to bridge the gap. Moreover the lemmas appearing in types will “go away” if you plug in any finite number for the dimension. This makes the library a drop-in replacement of previously defined sphere in most cases. The only missing feature is that, while non-dependent elimination rules are derived from the dependent ones, the non-dependent computation rules for loops are not. A 100% drop-in replacement should have all non-dependent rules derived from dependent counterparts.

Technical Discussion

Towers of Loops

Let’s set up the n-cell in spheres so that we can talk about computation rules. They are basically higher-order loops, that is, towers of loops:

S-endpoints⇑ 0 base = lift tt
S-endpoints⇑ (suc n) base = (S-endpoints⇑ n base , S-loop⇑ n base , S-loop⇑ n base) 

S-loop⇑ 0 base = base
S-loop⇑ (suc n) base = refl (S-loop⇑ n base)

whose data are filled by two mutually recursive functions where n is the dimension. We can then fake the loop (n-cell) constructor by a postulation in Agda:

postulate
  loopⁿ : ∀ n → Path⇑ n (S-endpoints⇑ n (baseⁿ n))

The elimination rule for spheres is shown below, where S-endpoints[dep]⇑ is the dependent loop tower parametrized by the mapped base point. This is probably not so surprising if you are familiar with S¹ in Agda. The scary type in the middle means “the path built from the dependent form of the loop and the data for the base point”. For S¹ this is simply subst P loop¹ pbase ≡ pbase. The last line establishes the definitional equality for the base point.

Sⁿ-elim : ∀ {ℓ} n (P : Sⁿ n → Set ℓ) (pbase : P (baseⁿ n))
          → Path[dep]⇑ n P (loopⁿ n) (S-endpoints[dep]⇑ n P (baseⁿ n) n P pbase)
          → ∀ x → P x
Sⁿ-elim n P pbase _ baseⁿ′ = pbase

Fix the Type Mismatch in Computation Rules

We already have computation rules for base points for free (by Dan’s trick). The remaining type mismatch mentioned above is due to lack of (definitional) communicativity between “building towers” and “applying functors” in Agda. That is, we want to show that building a tower of loops as above, and then mapping the whole tower to another space, is equivalent to mapping the base point to the target space first and then building up the tower right within that space. This is done by an induction on the dimension; we walk down the tower by repetitively applying the J rule.

Again (as in Part I), the way the tower is presented is important. It is difficult, if not impossible, to walk down the tower if the tower is upside down—that the outermost loop is the loop in the lowest dimension. My ordering (which exposes the path (or the loop here) in the highest dimension) makes this task easy. The particular induction here involves two mutually recursively defined functions to deal with different data in the tower. This is somewhat expected as we adopted mutually recursive functions to build towers as well.

One feature is that the usage of the J rule within this lemma is carefully arranged so that, in any given finite dimension, the proof will be definitionally equivalent to refl. This means that any previous code that depends on a sphere in some fixed dimension will not notice this artifact.

Non-dependent Rules

The final note is about the definition and derivibility of non-dependent rules.

For non-dependent elimination rules, we have to show that, a non-dependent tower is equivalent to a dependent tower with a “constant” type family. (Sorry but I am not sure about the accurate terminology here.) This can be achieved by the same technique—walking down the tower to the ground.

The type of the non-dependent computation rule has the same type mismatch issue, and can be solved by the technique mentioned above—but for non-dependent constructs this time.

On the other hand, the derivability of the non-dependent computation rule seems quite involved and so I have not finished it. Fortunately, I am not aware of any code that depends on the assumption that the non-dependent computation rule is derived from the dependent version.

Thanks to many people (Dan Licata, Bob Harper, etc) for helping me overcome my laziness.

Posted in Code, Higher Inductive Types | Leave a comment

On h-Propositional Reflection and Hedberg’s Theorem

Posted on 27 November 2012 by Nicolai Kraus

Thorsten Altenkirch, Thierry Coquand, Martin Escardo, Nicolai Kraus

Overview

Hedberg’s theorem states that decidable equality of a type implies that the type is an h-set, meaning that it has unique equality proofs. We describe how the assumption can be weakened. Further, we discuss possible improvements if h-propositional reflection (“bracketing”/”squashing”) is available. Write X* for the h-propositional version of a type X. Then, it is fairly easy to prove that the following are logically equivalent (part of which Hedberg has done in his original work):

X is h-separated, i.e. ∀ x y → (x ≡ y)* → x ≡ y
X has a constant endofunction on the path spaces, i.e. we have a function f: (x y: X) → x ≡ y → x ≡ y and a proof that f x y is constant for all x and y
X is an h-set, i.e. ∀ x y: X → ∀ p q: x ≡ y → p ≡ q

We then state the three properties for arbitrary types instead of path spaces. For a type A, the first two statements become

A is h-stable, i.e. A* → A
A has a constant endofunction, i.e. f: A → A and a proof of ∀ a b → fa ≡ fb

Clearly, the first statement is at least as strong as the second, but somewhat surprisingly, the second also implies the first. The proof of this fact is non-trivial.
In this blog post, we mainly talk about the mentioned results and try to provide some intuition. This is actually only a small part of our work. Many additional discussions, together with formalized proofs, can be found in this Agda file. Thanks to Martin, it is a very readable presentation of our work.

Generalizations of Hedberg’s Theorem

Having this proof of Hedberg’s Theorem in mind, the essence of the theorem can be read as:

(i) If we can construct an equality proof whenever we have h-propositional evidence that there should be one, then the type is an h-set.

Here, we call a type h-propositional (or an h-proposition) if all its elements are equal. Intuitively, decidable equality is much stronger than the property mentioned above: If we have a function dec that decides equality and x, y are two terms (or points), we do not even require evidence to get a proof that they are equal. Instead, we can just apply dec to get such a proof or the information that none exists.

It is therefore not surprising that Hedberg’s theorem can be strengthened by weakening the assumption. For example, a proof of ¬¬ x ≡ y could serve as evidence that x, y are equal; and indeed, if we know that a type is separated, i.e. that we have ∀ x y → (¬¬ x ≡ y) → x ≡ y, then the type is an h-set. This requires a weak form of extensionality (to show that ¬¬ x ≡ y is an h-proposition) and the controverse is not true.

In the presence of h-propositional reflection, we can do much better. We define h-propositional reflection as an operation _* from types to h-propositions (viewed as a subsets of types) that is left adjoint to the embedding, i.e. we have a universal property. These are Awodey’s and Bauer’s bracket types: The idea is that, given a type X, the type X* corresponds to the statement that there exists an inhabitant of X (we say that X is h-inhabited if we have p: X*). We always have the map η: X → X*. From X*, we do usually not get X, but if we could prove an h-proposition from X, then X* is sufficient. It is natural to consider h-propositional reflection in our context, because the informal notion “h-propositional evidence, that a type is inhabited” can now directly be translated. We call a type satisfying (i) in this sense h-separated: h-separated X = ∀ x y → (x ≡ y)* → x ≡ y.

In Hedberg’s original proof, it is shown that a constant parametric endofunction on the path spaces is enough to ensure that a type is an h-set. For a function f, we define that f is constant by constant f = ∀ x y → fx ≡ fy. As already mentioned above, it is fairly straightforward to show:

Theorem. For a type X, the following properties are logically equivalent:

X is h-separated, i.e. ∀ x y → (x ≡ y)* → x ≡ y

X has a constant endofunction on the path spaces, i.e. we have a function f: (x y: X) → x ≡ y → x ≡ y and a proof that f x y is constant for all x and y

X is an h-set, i.e. ∀ x y: X → ∀ p q: x ≡ y → p ≡ q

For this reason, we consider h-separated X → h-set X the natural strengthening of Hedberg’s theorem. The assumption is now the exact formalization of the condition in (i), the assumption is as weak as it can be (as it is necessary) and, in particular, it is immediately implied by Hedberg’s original assumption, namely the decidable equality property.

H-propositional Reflection and Constant Endofunctions

The list of equivalent statements above suggests that one could look at these statements for an arbitrary type A, not only for the path spaces. Of course, they do not need to be equivalent any more, but they become significantly simpler:

A is h-stable, i.e. A* → A
A has a constant endofunction, i.e. f: A → A and a proof of ∀ a b → fa ≡ fb
A is an h-proposition, i.e. ∀ a b: A → a ≡ b

For the third, it is pretty clear what this means and it is obviously strictly stronger than the first and the second. If A is h-stable, we get a constant endofunction by composing η: A → A* with A* → A. However, it is nontrivial whether a type with a constant endofunction is h-stable. Somewhat surprisingly, it is.

But let us first consider the question we get if we drop the condition that we are dealing with endofunctions. Say, we have f: X → Y and a proof c: constant f. Can we get a function X* → Y?
Consider the chaotic equivalence relation on X, which just identifies everything: x ~ y for all x and y, which is h-propositional (~: X → X → hProp with x ~ y = True for all x and y, if we want). According to the usual definition of a quotient, our constant map f can be lifted to X/~ → Y. So, what we asked can be formulated as: Does X* have the properties of X/~? If Y is an h-set, this lifting exists (Voevodsky makes use of this fact in his definition of quotients), but otherwise, our definition of constant is too naïve, as it involves no coherence conditions at all. If we know that Y has h-level n, we can try to formulate a stronger version of constant that solves this issue. This could be discussed at another opportunity. With the naïve definition of constant, we would have to make a non-canonical choice in X, but f only induces an “asymmetry” in Y.

Let us get back to the case where f is a constant endofunction. We still do not have the coherence properties mentioned above, but the asymmetry of Y is now an asymmetry of X and, somewhat surprisingly, this is sufficient. We have the following theorem:

Theorem. A type X is h-stable (X* → X) iff it has a constant endofunction.

Note that the direction from right to left is easy. For the other direction, we need the following crucial lemma:

Fixpoint Lemma (N.K.). If f: X → X has a proof that it is constant, then the type of fixed points Σ(x:X) → x ≡ fx is h-propositional.

Let us write P for the type Σ(x:X) → x ≡ fx. A term of P is a term in X, together with the proof that it is a fixed point. With the lemma, we just have to observe that there is the obvious map X → P, namely λx → (fx , constant x fx) to get, by the universal property of *, a map X* → P. Composed with the projection map P → X, this gives us the required map showing that X is h-stable.

To prove the lemma, we need the following two observations. For both, we assume that X, Y are types and x,y: X terms. Further, we write p • q for trans p q, so that this typechecks if p: x ≡ y and q: y ≡ z. We use subst (weak version of J) and cong (to apply functions on proofs) in the usual sense.

Observation 1. Assume h, k: X → Y are two functions and t: x ≡ y as well as p: h(x) ≡ k(x) are paths. Then, subst t p is equal to (cong h t)⁻¹ • p • (cong k t).

This is immediate by applying the equality eliminator on (x,y,t). We will need this fact for a proof of type t : x ≡ x, but this required special case cannot be proved directly.

The second observation can be considered the key insight for the Fixpoint Lemma:

Observation 2. If f: X → Y is constant, then cong f maps any proof of x ≡ x to reflexivity.

It is not possible to prove this directly. Instead, we formulate the following generalization: If c: constant f is the proof that f is constant, then cong f maps any proof p: x ≡ y to (c x x)⁻¹ • (c x y). This is immediate by using induction (i.e. the J eliminator) on (x,y,p), and it has the above statement as a consequence.

Proof (of the Fixpoint Lemma). Assume we have f: X → X, c: constant f and (x,p), (x',p'): Σ (x: X) → x ≡ fx. We need to show that these pairs are equal. It is easy to prove x ≡ x' by composing the proofs p: x ≡ fx, constant x x': fx ≡ fx' and (p')⁻¹: fx' ≡ x'. We call this proof p'': x ≡ x'. Clearly, we have that (x, subst (p'')⁻¹ p') and (x',p') are equal now, just by the proof p'' for the first component, and the equality of the second components is immediate. We choose to write q for the proof subst (p'')⁻¹ p'. Now, we are in a slightly simpler situation: We need to show that (x,p) and (x,q) are equal.

If we prove that the first components are equal using some proof t: x ≡ x, then what we need for the second components is p ≡ subst t q. Clearly, using refl for t would not work.

By Observation 1, our goal is equivalent to proving p ≡ t⁻¹ • q • (cong f t).
Using Observation 2, this simplifies to p ≡ t⁻¹ • q. Let us therefore just choose t to be q • p⁻¹. This completes the proof of the Fixpoint Lemma and the Theorem. □

As mentioned, there is a bunch of possible further questions and considerations, but for now, we want to conclude with a question that we are not so sure about anymore: Is h-propositional reflection definable in MLTT (with extensionality)? With heavy use of the Fixpoint Lemma, we have come fairly close to such a definition. It should not be possible, but is there a proof of that fact?

Posted in Code, Foundations | 17 Comments

On Heterogeneous Equality

Posted on 21 November 2012 by Mike Shulman

(guest post by Jesse McKeown)

A short narative of a brief confusion, leading to yet-another-reason-to-think-about-univalence, after which the Author exposes his vaguer thinking to derision.

The Back-story

In the comments to Abstract Types with Isomorphic Types, Dan Licata mentioned O(bservational)TT, originating in works of McBride, with Altenkirche, McKinna… One of the initially-strange features therein is a so-called "heterogeneous equality" type, which from my very cursory reading I see has something to do with coercing along equivalences. Of course, this piqued my curiosity and a short-while later I happened upon this book about using coq as a practical program verification assistant, by way of this section of the chapter "Equality".

Continue reading →

Posted in Uncategorized | 19 Comments

Homotopy Type Theory