Another Formal Proof that the Higher Homotopy Groups are Abelian

I have adapted Dan Licata’s Agda proof that the higher homotopy groups are abelian to Coq, and I have added a link to the code on the code page of this blog.

This entry was posted in Code. Bookmark the permalink.

4 Responses to Another Formal Proof that the Higher Homotopy Groups are Abelian

1. Mike Shulman says:

Nice! It looks simpler than I expected. I’m intrigued by your comment in the source that proving adjust_l (and, I presume, adjust_r) by induction didn’t give a term that was explicit enough. I’ve had a similar experience with the induction proofs of equiv_inv, equiv_inv_is_section, and equiv_inv_is_retraction, but I thought that maybe I was doing something wrong. It’s too bad if the convenient induction tactic has a tendency to produce proofs that aren’t good enough for further use. Are the proofs “really” different, or is Coq just not able to figure out that they’re the same?

I also have to repeat my suggestion that we say $\Omega^2$ rather than $\pi_2$ when that’s what we really mean. (-:

Thanks, Mike.

In fact, I was just able to prove the two proofs (i.e. paths) are homotopic to one another; see the code below.

What’s going on is that when it comes to Omega^2, the two endpoints of a path p are the same; so induction over p no longer works, and it become impossible to simplify j terms over paths. So one needs a description of the homotopy that doesn’t require unpacking a j-term.

The fact that “proofs” are far from irrelevant here — e.g. they can describe paths that one wants to reason about — makes me uneasy. The particularities of a proof can have an effect on future developments in ways that I still don’t fully understand. For example, Dan pointed out to me that his code only needs one “adjustment” (whereas I need adjust_l and adjust_r) because he used a different definition of concatenation/transitivity than Andrej did. Roughly, Andrej (proved transitivity “trans p q”) / (defined concatenation “p @ q”) by contracting both p and q, which has the effect that “id_path x @ idpath_x” is definitionally equal to “idpath x”. But if you prove it instead by contracting only the first, say, then you get the more useful property that “id_path x @ p” is definitionally equal to “p”. That better definition would have made my code a bit shorter.

Welcome to the wonderful world of proof relevance.

*****

Lemma adjust_l {A} {x y : A} {p q : x ~~> y} (R : p ~~> q) :
idpath x @ p ~~> idpath x @ q.
Proof. exact (idpath_left_unit p @ R @ !(idpath_left_unit q)). Defined.
(* induction R doesn’t given a term that is explicit enough. *)

Lemma adjust_l2 {A} {x y : A} {p q : x ~~> y} (R : p ~~> q) :
idpath x @ p ~~> idpath x @ q.
Proof. induction R. apply idpath. Defined.

Lemma test {A} {x y : A} {p q : x ~~> y} (R : p ~~> q) :
Fascinating! It doesn’t really bother me too much that these “proofs” are “relevant”, because as a homotopy theorist, I don’t call these things “proofs of theorems” but rather “constructions of paths.” And “obviously” when you construct a path, it can matter which path you construct. (-: But it does seem a little unfortunate that we have to pay attention to details like this.