In my study of Type Theory, the univalence axiom has been introduced as the statement that "Isomorphic structures are equal." I haven't learned how to define any algebraic, combinatorial, or topological structures in type theory yet. BUT I do know that there are times in math where it pays to think of isomorphic structures as distinct representation of the same isomorphism class. For example, even though $2\mathbb{Z} \cong 3\mathbb{Z}$, $\mathbb{Z}/2\mathbb{Z}\ncong\mathbb{Z}/3\mathbb{Z}$.
So, does the univalence axiom imply $\mathbb{Z}/2\mathbb{Z}\cong\mathbb{Z}/3\mathbb{Z}$? My guess is of course not, since this would probably create lots of problems, but then what am I missing in my understanding of the univalence axiom?
In order for $G/H$ to be a well defined object, it's not enough for $H$ to just be a group. It needs to be a (normal) subgroup of $G$. One way to phrase this in type theory, is that $H$ is a group together with an embedding $H \hookrightarrow G$. Then $2 \mathbb{Z}$ and $3 \mathbb{Z}$ are not isomorphic as subgroups of $G$, because an isomorphism would have to preserve all the structure, including the embeddings into $G$.
There is a "forgetful functor" from subgroups of $G$ to groups that just throws away the embedding. The images of $2 \mathbb{Z}$ and $3 \mathbb{Z}$ are then equal, assuming univalence, because they are isomorphic as groups. But that's fine - it just says that the forgetful functor is not injective on objects. Similar things can even happen in set theory.