"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:S^1} P(x)$.

"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)$.