Homotopy type theory (HoTT) will have applications for both computer science and math. On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, applications include using type theoretic proof assistants, like Coq and Agda, to give formal, machine-verified, proofs of mathematical theorems. We’d like to show that HoTT is useful for formalizing homotopy theory and higher-dimensional category theory, and then that the ability to work up-to-equivalence is useful for other parts of math as well.

As a first example of the former, we can prove the well-known result that the higher homotopy groups of a topological space are all abelian.

Given a space `A` and a distiguished base point `base`, the *fundamental group* `π1` is the group of loops around the base point. `π1` has, as elements, the loops at `base`—paths from the base point to itself—with the group multiplication given by composition, and the identity element by the identity path. However, to satisfy associativity and unit, the paths must be quotiented by homotopy.

However, the homotopies, or deformations of paths, themselves have some structure, and we can look at the *second fundamental group* `π2`, which is the same construction “one level up”: take the base point to be the identity loop at the original base point `base`, and then look at the homotopies from this loop to itself (again quotiented by higher homotopies).

It turns out that the second fundamental group, and all higher ones obtained by iterating this construction, are abelian. The way we’ll prove this is to show that there are two different notions of composition on them, which have the same unit and satisfy an interchange law, so the result follows from the Eckmann-Hilton argument. What are the two notions of compostion? The first is the multiplication from `π2`, which is just composition/transitivity of homotopies/deformations. The second uses composition of loops one level down (which explains why the fundamental group is not necessarily abelian), and states that composition preserves deformability. Namely, if you have four loops around `base`, `p q p' q'` and a deformation from `p` to `p'` and a deformation from `q` to `q'`, then you can compose these to give a deformation from `q ∘ p` to `q' ∘ p'`. Now, take all four loops to be the identity, in which case we have an operation that takes two elements of `π2` (i.e. two deformations from the identity loop to itself) and gives back a third (by the unit laws, id ∘ id = id).

Next, we are going to formalize this proof in type theory. In particular, I will use Agda, though the proof could easily be translated to Coq.

Here are the basic definitions:

module FundamentalAbelian (A : Set) (base : A) where π1El : Set π1El = base ≃ base π2El : Set π2El = _≃_{π1El} Refl Refl _∘_ : π2El → π2El → π2El p ∘ q = trans q p _⊙_ : π2El → π2El → π2El a ⊙ b = resptrans b a ⊙-unit-l : (p : π2El) → (Refl ⊙ p) ≃ p ⊙-unit-l p = resptrans-unit-r p ⊙-unit-r : (a : π2El) → (a ⊙ Refl) ≃ a ⊙-unit-r a = trans (resptrans-unit-l a) (trans-unit-l a) interchange : (a b c d : _) → ((a ∘ b) ⊙ (c ∘ d)) ≃ ((a ⊙ c) ∘ (b ⊙ d)) interchange a b c d = trans-resptrans-ichange _ _ d _ c _ _ b _ a

We define a module parametrized by a set `A` (Agda uses the word `Set` for ‘type’) and a term `base` of that type: the proof works for any space and base point. The type `π1El` (the elements of π1) is defined to be the loops at `base`, represented using the identity type `M ≃ N`, which is defined in a library. Similarly, the elements of π1 are the loops (at type `π1El`) at reflexivity. The two notions of composition discussed above are defined in the identity type library, with ∘ defined by transitivity, and ⊙ defined by `resptrans`–the proof that transitivity respects equivalence.

`⊙-unit-l` proves the left unit law for ⊙. The way to read this declaration is (1) ⊙-unit-l is a term of type `(p : π2El) → (Refl ⊙ p) ≃ p` (where `(x : A) → B` is Agda syntax for a Pi-type), and (2) it is defined to be the term `λ p → resptrans-unit-r p`. That is, it is implemented by a straightforward application of a lemma in the identity type library. `⊙-unit-r` is similar, except it takes two lemmas to prove: the general `resp-trans-unit-l` states that `resptrans Refl a` is equal to `a` composed with proofs that cancel `trans - Refl` (transitivity with reflexivity on this side is propositionally but not definitionally the identity, for the way I have defined transitivity); however, in this case, these transitivities cancel, because the base point is reflexivity.

The middle-four interchange law states an interaction between the two notions of composition, which is key to the proof below. It is proved using an application of a lemma from the library.

Now, we can give a simple formalization of the Eckmann-Hilton argument, which proves that the two compositions are the same, and abelian:

same : (a b : π2El) → (a ∘ b) ≃ (a ⊙ b) same a b = (( a ∘ b) ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-r a)) 〉 ((a ⊙ Refl) ∘ b) ≃〈 resp (λ x → (a ⊙ Refl) ∘ x) (sym (⊙-unit-l b)) 〉 ((a ⊙ Refl) ∘ (Refl ⊙ b)) ≃〈 sym (interchange a Refl Refl b) 〉 ((a ∘ Refl) ⊙ (Refl ∘ b)) ≃〈 resp (λ x → x ⊙ (Refl ∘ b)) (trans-unit-l a) 〉 (a ⊙ (Refl ∘ b)) ≃〈 resp (λ x → a ⊙ x) (trans-unit-r b) 〉 (a ⊙ b) ∎) abelian : (a b : π2El) → (a ∘ b) ≃ (b ∘ a) abelian a b = (a ∘ b) ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-l a)) 〉 ((Refl ⊙ a) ∘ b) ≃〈 resp (λ x → (Refl ⊙ a) ∘ x) (sym (⊙-unit-r b)) 〉 ((Refl ⊙ a) ∘ (b ⊙ Refl)) ≃〈 interchange Refl b a Refl 〉 ((Refl ∘ b) ⊙ (a ∘ Refl)) ≃〈 resp (λ x → x ⊙ (a ∘ Refl)) (trans-unit-r b) 〉 (b ⊙ (a ∘ Refl)) ≃〈 resp (λ x → b ⊙ x) (trans-unit-l a) 〉 (b ⊙ a) ≃〈 sym (same b a) 〉 (b ∘ a) ∎

The proof is exactly the textbook Eckmann-Hilton argument. We use a notational trick to write the proof as a sequence of steps `x ≃〈 p 〉y`, which is read `x` is equivalent to `y` by `p`. To prove that the compositions are the same, we expand using the unit laws, apply interchange, and then contract. To prove that they are abelian, we expand using the unit laws, apply interchange, and contract, which swaps the order but also swaps the composition; so `same` gives the result. In the proofs, `resp` is a general compatibility lemma, which lifts an equation into a context (given by the function in its first argument).

The thing to take away from this post is that, after developing some libraries for identity types, we were able to use a simple, clean transcription of the Eckmann-Hilton argument to give a formal proof of the result. In the next post, I’ll talk about the lemmas we used from the identity type library.

Technical caveat: following the discussion here (if I have understood it correctly; if not please correct me), what this theorem really states is that composition in the *loop space* is abelian, up to higher homotopies (because the statement of the theorem itself uses the identity type). This is slightly different than stating that the fundamental group is abelian. The difference is that the loop space is itself a whole higher-dimensional space, with “external” higher-dimensional homotopies, whereas the fundamental group theorem talks about the *group* whose elements are *paths quotiented by homotopy*. Our theorem statement is like saying that two numbers are congruent mod k, whereas the theorem about fundamental groups is like saying that two elements of Z/kZ are equal. Of course, it’s easy to go between these, but to state the latter version in type theory, we will need a form of *quotient types* that lets one quotient by higher dimensional structure to obtain a lower-dimensional type.

The code for this post is here, for now, until I make a GitHub repository. Thierry Coquand and Nils Anders Danielsson have a proof here, but it seems to use a different argument than Eckmann-HIlton.

Nice! I think you understood the discussion about loop spaces correctly. Given that the theorem is really about loop spaces, why not use the homotopically correct notation rather than ?

I would be surprised if Thierry and Nils’ proof is materially different from the Eckmann-Hilton argument. Glancing at it briefly, it looks about the same but just keeping track of all the “unitor” isomorphisms, although it’d take some time to puzzle out exactly what everything means.

One day, maybe someone will write a proof assistant that understands higher-dimensional pasting or string diagrams directly. (-:

The statement for certainly follows from the proof given, and since the higher homotopy groups are more familiar to non-specialists, it seems reasonable to me to state it this way in this forum.

I just meant that in the Agda file itself, the object defined as “” is actually . Certainly, when explaining it to nonspecialists it makes sense to talk about homotopy groups, but in the actual code we can be precise, no?

I basically agree with you, Mike, and in a ‘real’ development I would probably use the loop space notation. Here, I used the fundamental group notation because a couple of people that I explained this to knew about fundamental groups (from an undergrad topology course) but not loop spaces.

Re: Thierry and Nisse’s proof: from a very cursory glance, I couldn’t find the definition of ‘resptrans’–maybe it’s inlined? That’s what made me think it was a different argument.

sure.

It looks to me like rather than proving directly that is commutative, Thierry and Niesse prove a bit more abstractly first that given any type equipped with a binary operation that has a 2-sided unit e, the composition of endo-paths of e is commutative. This is a well-known equivalent version of the Eckmann-Hilton theorem. Then they apply that to the endo-paths of the basepoint of a type X, equipped with the composition operation, to deduce that is commutative. I think the equivalent of your

resptransmay be hiding in their operations calledcongandcong._{2}Ooh, you’re right. On a slightly longer glance, I see that

`lc`

and`rc`

are defined in terms of`cong`

, which is definitely the equivalent of`resptrans`

I think one of the most interesting things about these proofs is the way they use a sort of “synthetic” reasoning about path-spaces: rather than treating them as maps from the unit interval and reparameterizing, etc., one uses the the Id-elim rule as a (weak) universal property of the path space itself — what Andrej Bauer has termed “path induction”. This is a proof method that — to my knowledge — is not used in traditional homotopy theory (although it is, to be sure, related to weak factorization system lifting properties).

It’s use is based on the reading of the Id-type as (some sort of weak) identity relation, generalizing from predicate logic to the constructive setting, where one has to also keep track of “evidence” or proof terms. In fact, the Id-elim rule itself can be recognized as essentially Lawvere’s adjoint rule for equality, but decorated with proof-terms.

I would expect this (new?) point of view should shed a different light on other constructions in classical homotopy theory as well. Another simple example is the interpretation of fibrations as “predicates” — i.e. families of (proof-relevant) propositions that respect “identity”.

I agree, to a certain extent. In one of my nCafe posts, I thought of writing something like “in this way the type-theoretic proofs that equality is transitive and symmetric can be identified with the model-category-theoretic proofs that homotopies can be composed and reversed,” but then when I unraveled the proofs, as far as I could tell they were actually different! That surprised me. Of course, it’s not immediately clear that path induction will always

workin traditional homotopy theory, since a weak factorization system has to have certain very special properties to model identity types.On the other hand, it seems that once we use path induction to prove the basic facts about composition of paths, the Eckmann-Hilton argument is proven in the same way as in homotopy theory.

I think the correct level of generality is: if for a weak factorisation system (L,R) you assume that the L-maps are stable under pullback along the R-maps—as in, e.g., R=Kan fibrations of simplicial sets, or R=Hurewicz fibrations of topological spaces—then the homotopy relation defined in terms of path objects will be symmetric and transitive at any fibrant object, with the same proof as the type-theoretic one.

Yes, certainly. Whereas there is a different proof that works in any category of fibrant objects.

Pingback: Just Kidding: Understanding Identity Elimination in Homotopy Type Theory | Homotopy Type Theory

Pingback: Another Formal Proof that the Higher Homotopy Groups are Abelian | Homotopy Type Theory