With Agda version 2.6.0 close to being released, I decided to experiment with cubical Agda.
Now that the documentation for cubical Agda is available, it should be easier to start experimenting. I first tried to formalise Frumin, Geuvers, Gondelman, and van der Weide's Finite Sets in Homotopy Type Theory. However I got stuck trying to write the very first function when I had to figure out what a path's image was. Time to go back to basics!
My attempt to boil down the problem I was facing resulted in List⁰. It is a higher inductive type of strange lists: we have the two usual list constructors, together with a path saying that a non-empty list is equal to its tail.
data List⁰ (A : Set) : Set where [] : List⁰ A _∷_ : A → List⁰ A → List⁰ A del : ∀ x e → x ∷ e ≡ e
Hopefully, this mix of the familiar and the new will let us build on our old intuitions to understand new concepts. We can start by revisiting a function we know very well in the list case.
We define append by recursion on the first list. The first two cases are similar to what one would do in Haskell (or vanilla Agda): if the first list is empty, we return the second one; and if it has a head and a tail, we cons the head and the result of the recursive call on the tail. But there is also a third case: List⁰ is a higher inductive type and that means that we need to explain how append acts on paths!
_++_ : (e f : List⁰ A) → List⁰ A [] ++ f = f (x ∷ e) ++ f = x ∷ (e ++ f) del x e i ++ f = ?
Because the function _++_ acts on elements of List⁰ A, we need its first argument to be of type List⁰ A. For this reason, the case mentions del x e i: a value at position i along the line of type x ∷ e ≡ e described by del. The type of the hole is List⁰ A but it does not mean that we can put just about any expression in: there are side conditions!
These sides conditions can be understood from a very practical point of view: if i gets instantiated to either i0 or i1, the value of del x e i ++ f should not depend on whether we evaluate _++_ first and then instantiate i, or the converse. To guarantee that evaluation is confluent, Agda demands that both reductions lead to judgmentally equal values.
Understanding where these constraints come from, we can compute them. Remembering that if p has type a ≡ b then p i0 = a and p i1 = b:
i = i0 ⊢ del x e i ++ f { del x e i0 = x ∷ e } = x ∷ e ++ f { unfold _++_ } = x ∷ (e ++ f) i = i1 ⊢ del x e i ++ f { del x e i1 = e } = e ++ f
So, the expression we pick to fill in the List⁰ A will need to be equal to x ∷ (e ++ f) if i is i0 and e ++ f if i is i1. Observing that del x (e ++ f) has type x ∷ (e ++ f) ≡ e ++ f, we pick the following solution:
del x e i ++ f = del x (e ++ f) i
Agda performs the checks we have mentioned earlier and sees that our solution is indeed compatible with the equations we already had. We now have a fully-defined function. Time to prove some of its properties!
Just like for lists, we can prove that [] is a neutral element for the binary operation _++_. That is to say that both [] ++_ and _++ [] are the identity function. This should not be too much work but it will get us the opportunity to think about what happens in the del case. We will then prove a more complex result: given that del allows us to peel-off the head of a non-empty list, we should be able to prove that we can ``cancel'' append, that is to say that e ++ f is equal to f.
The left identity holds by computation: the definition of append itself declares that [] ++ e should reduce to e. We can use refl to prove the goal like we would do in vanilla Agda. The main difference here being that refl is not a constructor: it is the constant function which given any value in the interval returns e.
++-idˡ : (e : List⁰ A) → [] ++ e ≡ e ++-idˡ e = refl
The right identity requires a bit more work: given that append is defined by recursion on its first argument, we need to proceed by induction on it. The first two cases are what you would expect from the proof of a similar result on lists.
++-idʳ : (e : List⁰ A) → e ++ [] ≡ e ++-idʳ [] = refl ++-idʳ (x ∷ e) = cong (x ∷_) (++-idʳ e) ++-idʳ (del x e i) = ?
The last case is not a lot more complicated, at least at first glance:
i = i0 ⊢ ++-idʳ (del x e i) { del x e i0 = x ∷ e } = ++-idʳ (x ∷ e) { unfold ++-idʳ } = cong (x ∷_) (++-idʳ e) i = i1 ⊢ ++-idʳ (del x e i) { del x e i1 = e } = ++-idʳ e
We can easily verify that cong (λ e → del x e i) (++-idʳ e) does collapse to the right expressions when we set i to either i0 or i1 thanks in part to the fact that cong (λ x → x) p is definitionally equal to p. This leads us to the following completed definition:
++-idʳ : (e : List⁰ A) → e ++ [] ≡ e ++-idʳ [] = refl ++-idʳ (x ∷ e) = cong (x ∷_) (++-idʳ e) ++-idʳ (del x e i) = cong (λ e → del x e i) (++-idʳ e)
We can now move on to a more difficult proof.
Given that a non-empty list is declared equal to its tail it should be possible to prove that if we append two lists, the result is equal to the second one alone. The intuition being that we can repeatedly use del to consume all of the elements in the first list. Formally, this gives us the type:
dels : (e f : List⁰ A) → e ++ f ≡ f
Remarking once more that append is defined by recursion on its first argument, we proceed by induction on it. The first case is easily dealt with: it is precisely the left identity law for append which we know holds definitionally. For uniformity with the upcoming case, we eta-expand refl and write [1]:
dels [] f j = f
The second clause demands an equality proof between x ∷ e ++ f on the one hand and f on the other. We could use transitivity to combine a call to del taking us from x ∷ e ++ f to e ++ f and then use the induction hypothesis to conclude. However it turns out that we can find a more compact proof by defining the path explicitly. We write:
dels (x ∷ e) f j = del x (dels e f j) j
We let the reader check that when j is i0 we do get x ∷ e ++ f whilst making j equal to i1 takes us to f. We are now left with the last clause. We need a term of type del x e i ++ f ≡ f which satisfies the usual two side conditions stating that when we make i either i0 or i1, it is compatible with the previous clauses.
i = i0 ⊢ dels (del x e i) f j { del x e i0 = x ∷ e } = dels (x ∷ e) f j { unfold dels } = del x (dels e f j) j i = i1 ⊢ dels (del x e i) f j { del x e i1 = e } = dels e f j
It is hard to give an intuition for the jump from these constraints to the solution. One thing we can notice is that dels e f j is the right hand side of the equality proved by del x (dels e f j). So we need to somehow get a term which is equal del x (dels e f j) j when i is i0 and collapses to del x (dels e f j)'s right hand side when i is i1.
The key idea in cubical Agda which will help us here is the fact that elements of the interval form a De Morgan algebra. We can use the interval value i ∨ j: when i is i0, we get j back and when i is i1, i ∨ j collapses to i1.
The reader can check that λ j → del x (dels e f j) (i ∨ j) proves the equality del x e i ++ f ≡ f and that it reduces to the right expressions when i is set to either of the interval's extremities. Putting everything together, we get the following definition:
dels : (e f : List⁰ A) → e ++ f ≡ f dels [] f j = f dels (x ∷ e) f j = del x (dels e f j) j dels (del x e i) f j = del x (dels e f j) (i ∨ j)
It took me about ten hours total to formalise the content of this post, most of it spent on dels. Once I understood the origin of the side conditions one has to deal with in the cases involving del x e i, it finally clicked and things felt easier. I hope this post makes the confluence imperative behind these side conditions clear and really drills down the importance of computing them.
I would like to conclude this post by thanking Nils van der Weide and Dan Frumin for sharing my misery when banging my head against these simple-looking problems as well as the insightful discussions that ensued.