Role of univalence in homotopy group calculations

Question

This book has a section with proofs of the fact $\pi_1(S^1)=\mathbb Z$ using the univalence axiom. They are a bit too technical for me at the moment to read, but I want to understand the following (vague but conceptual) question:

What is the role of the univalence axiom in these proofs?

Usually, univalence is motivated with a slogan like "isomorphic structures are equal". However, it seems the application of univalence in the proofs of $\pi_1(S^1)=\mathbb Z$ must be of a completely different kind than "treating isomorphic algebraic structures as the same". So I really would like to get a hint at how univalence can be relevant to such concrete questions, as a motivation for reading the proofs in more detail.

Answer 1

Let's start with an easier question: How do we know that loop is not equal to refl in $\pi_1(S^1)$?

By the universal property of $S^1$ this is exactly saying that there exists some type $T$ and some $t:T$ and some loop $p:t=t$ which is not trivial. This means I want some type where it's easy to write down paths, but where it's also easy to tell if paths aren't equal to each other. Univalence gives a type that's great for this, namely the universe! The paths in the universe are just functions and you can show two functions are not equal by just showing they're not equal on some input.

So just look $\mathbb{Z}: U$ and $\mathrm{ua}(\mathrm{succ}): \mathbb{Z} = \mathbb{Z}$. This is clearly not refl because it sends $0$ to $1$ which is not $0$. Now we're done!

I think of checking $\pi_1(X) = G$ as having four parts, constructing generating loops, constructing relations, checking the generators generate, and checking that there's no additional relations. The first two of these parts can be done without univalence (and they're much nicer to do in Globular than in HoTT implementations). What I explained above is why univalence is important in checking that there's no additional relations. What I find a lot more subtle is how univalence also allows you to check that the generators generate. Why the generators generate is the real magic of the encode/decode method, and I'm not sure I can explain it the way I want to in just a MO answer.

Answer 2

"Isomorphic structures are equal" is a cute slogan, but it sometimes gets in the way because it sounds like it's saying that it forces isomorphic structures to be related by the pre-existing notion of "equality". What univalence actually does is to change the meaning of "equality" so that in the case of structures it coincides with the notion of isomorphism. Moreover, this coinciding is not just as a property but as a structure: since two structures can be isomorphic in more than one way, they can now also be equal in more than one way. In turn, this means that we must regard types now as (higher) groupoids rather than sets.

This is where the relevance to $\pi_1(S^1) = \mathbb{Z}$ comes from. The definition of $S^1$ in these results is essentially as a colimit: the coequalizer of the two maps $1\rightrightarrows 1$. In the category of sets, that coequalizer is just $1$ again, so that in particular "$\pi_1(S^1) = \mathbb{Z}$" is false. But in the (2-)category of groupoids, the coequalizer is nontrivial, and indeed satisfies $\pi_1(S^1) = \mathbb{Z}$. Univalence is thus what ensures we are working in a category of groupoids rather than a category of sets.

More concretely, the definition of $S^1$ has a "mapping-out" universal property, whereas $\pi_1(X)$ is (roughly speaking) about a "mapping in" property ("loops" drawn in $X$). Univalence allows us to deduce "mapping in" results from "mapping out" properties by using the universal property to construct a map $out$ of $S^1$ into the universe $\mathcal{U}$, and then turning a type family $P : S^1 \to \mathcal{U}$ into an object $\sum_{x:S^1} P(x)$ of the slice category over $S^1$ (which therefore maps into $S^1$). The reason we need univalence is that the universal property for mapping out of $S^1$ refers to equalities in the target, while univalence is what tells us about the equalities in $\mathcal{U}$.

This can be compared to similar results about "mapping in" properties of "lower inductive types" using a not-necessarily univalent universe. For instance, we prove $0\neq 1$ in $\mathbb{N}$ in a similar way, by using the universal property of $\mathbb{N}$ to construct a map into $\mathcal{U}$ and then passing to $\sum_{x:\mathbb{N}} P(x)$.

Answer 3

This is essentially the same content as earlier answers, but I’ll try to emphasise the aspect OP is asking about a bit more explicitly. $\newcommand{\Z}{\mathbb{Z}}$I’ll use the terminology of “paths” rather than “equalities”, to emphasise the space-like viewpoint.

• Classically, how do you investigate the structure of a free group, or a group presented by generators and relations? In particular, how do you know it’s non-trivial? You look at actions or representations of it — concretely presented groups, into which the presented group maps.

• The circle $S^1$ is defined as the type freely generated by a point and a loop at that point. $\pi_1(S^1)$ is the total type of loops at the basepoint. There’s a clear map $\Z \to \pi_1(S^1)$, by taking integer powers of the generating loop. But how do you show this is non-trivial? Since it’s a freely presented structure, you need to find maps into concretely presented types.

• Univalence says that paths between types correspond to equivalences between them. It follows fairly directly that paths between types-with-structure correspond to structure-preserving-equivalences — e.g. paths in the type of groups correspond to group isomorphisms.

• Take $\Z$, equipped with the successor endomorphism $s$. As a type-with-endomorphism $(\Z,s)$, it has $\Z$-many automorphisms, the integer powers of $s$ — you can calculate this in HoTT exactly the same way you would calculate it classically. By univalence, it follows that it has $\Z$-many paths to itself, all the integer powers of the basic loop corresponding to $s$. $\newcommand{\TyEnd}{\textrm{TyEnd}}$ In other words, $\pi_1(\TyEnd,(\Z,s)) \cong \Z$, where $\TyEnd$ is the type of types-with-endomorphism.

• So the universal property of $S^1$ gives a map into $\TyEnd$, taking its basepoint to $(\Z,s)$ and its generating loop to (the path corresponding to) $s$. This shows that the $\Z$-many powers of the loop in $\pi_1(S^1)$ must be distinct, since they get mapped to the automorphisms of $(\Z,s)$, which we know are distinct. (And with a little more work in similar tools, we can show the map $\Z \to \pi_1(S^1)$ is surjective.)

So the take-home in all this is: $S^1$ is the free type-with-a-loop. So to investigate its structure (in particular, $\pi_1(S^1)$), we want to find types with non-trivial loop spaces, or better still, where we can calculate loop spaces explicitly. Univalence tells us that loops in types of types-with-structure correspond to automorphisms of such types-with-structure; so it gives us types where there are interesting loop spaces that we can calculate explicitly.