Running Spheres in Agda, Part I

Introduction

Where will we end up with if we generalize circles S¹ to spheres Sⁿ? Here is the first part of my journey to a 95% working definition for arbitrary finite dimension. The 5% missing part is that the non-dependent elimination rule for Sⁿ is not (completely) derived from the dependent elimination rule.

There are two common ways to encode Sⁿ as an higher-inductive type: One consists of a 0-cell and an n-cell; for example, S¹ can be modelled as a base (the 0-cell) plus a loop (the 1-cell). The other is to have complement two cells from dimension 0 to dimension n; for example, S¹ can be viewed as two points (two 0-cells) along with two distinct paths (two 1-cells) connecting them.

In either case we need the ability to define cells in an arbitrary finite dimension. This is usually done by adding a homotopy (path) in that dimension. In this post I will present a way to specify those paths.

Folding the Points

A path consists of two end points. For higher paths those two end points are themselves paths sharing the same end points. By induction a path in dimension n is indexed by a list of pairs of end points in all lower dimensions, from dimension 0 to dimension (n-1). Let’s first define a type family (or bundle), Endpoints, indexed by the dimension and the base space, to hold these points. For paths in dimension 0 no end points are needed. For dimension 1 it is simply a pair of points in the base space. For dimension (n+1) it is tempting to define it as a pair of points, say x and y, in the base space, along with end points in higher dimensions starting from the base type x ≡ y (path x y). That is, Endpoints of dimension n and base type x ≡ y (path x y). The following is the Agda implementation with universe polymorphism: Note that ⊤ is the unit type and ↑ is the lifting operator for the lack of implicit cumulativeness of universes in Agda.

This definition, however, has a serious problem. Our goal is the path connecting two end points in the highest dimension (n-1), but they are buried deeply inside nested tuples! I found it rather challenging, if not impossible, to extract those two points (and their type). An alternative approach is to change the associativity and expose end points in the highest dimension. This eventually leads to mutually recursive definitions of paths and end points: Endpoints of dimension (n+1) is a dependent tuple of Endpoints of dimension n and two paths connecting the end points exposed by it; a path is in turn indexed by the end points. Here is the Agda code: (It seems that the Coq equivalent requires more encoding tricks to overcome the restrictions Coq put on mutually recursive definitions.)

For brevity, I call a (possibly higher) path in dimension n along with all the end points from the base space as higher-order paths. A 0-order path is equivalent to a point, and an 1-order path is equivalent a normal path. I am all ear about a better terminology for this.

Dependent Higher-order Paths

We need two more gadgets before moving to Sⁿ. One is dependent higher-order paths—higher-order paths in which all the end points and the path are parametrized by the corresponding end points and the path in another higher-order path. The other is the binary operator to construct such a higher-order path from a higher-order path and a functor from its base space to a total space. (For normal paths, it is called cong in my codebase inherited from Nils’, resp in Dan’s and map in the Coq HoTT repository.)

In intuition, our higher-order paths are towers of (possibly higher) paths; we would like to map each path in that tower to a path in the corresponding total space. The mapped paths also form a tower based at the corresponding space to the base space. Suppose there are two points, a₁ and a₂, and a path, p, from a₁ to a₂ in the base space A. Assume B is a bundle over A. We can pick two points, b₁ and b₂, in the fibers B a₁ and B a₂ as the corresponding points to a₁ and a₂. We can then pick a path from “transported b₁” (“subst p b₁” or “transport p b₁” or “p ! b₁”) to the point b₂ in the fiber B a₂ as the corresponding path to the path p. This process goes on to construct the whole tower—for example, the two points, b₁ and b₂, together with the path, q, (in some sense) form a tower based at B. Here’s the Agda code:

This program walks through the end points to construct the new tower. This definition is more complex than the definition of (non-dependent) higher-order paths because here we need subst (or transport in the Coq repository) to transport points.

The next one is the operator that produces a dependent higher-order path from a higher-order path and a functor:

It has two parts: The first part constructs the tower of end points and the second part constructs the higher path. Note that the associativity we chose to fold the tower also simplifies the definition of this operation. The induction goes top-down instead of bottom-up, and so the outermost path should be the path in the highest dimension.

There is also a non-dependent version of this operator (in the sense that the fiber is constant over the base space). This is a generalization to the non-dependent version of cong (or Dan’s resp or map in the Coq repository) that works for normal paths.

We can show that, if we plug a constant fiber into the dependent operator, the result will be (homotopically) equivalent to the non-dependent version. The proof is done by induction on the dimension, where each induction step uses the J rule multiple times.

With these tools, we are ready to move to the next part! All the code is available at my GitHub repository (with some minor name changes).