Running Spheres in Agda, Part II

Running Spheres in Agda, Part II

(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.