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.
Best Answer
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.