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.