Here, Dan Licata writes:
[Univalence] can be used to build algebraic structures in such a way that isomorphic structures are equal (e.g. equality of groups is group isomorphism).
He writes something similar here:
A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal).
Now nLab writes:
A category is skeletal if objects that are isomorphic are necessarily equal; so this is a notion irredeemably violating the principle of equivalence of category theory.
Is there not a contradiction here? How can we claim that:
- skeletons violate the principle of equivalence
- univalence upholds it
when apparently, univalence implies that every category is skeletal?
Well, Homotopy Type Theory introduces some extraordinary equality, which approach requires special attention, and so the n-Lab article is a little bit out of this context, as it uses categories over some classical set theory, while HoTT defines its own 'precategories' and 'categories'.
For a motivating example, when we arrange four small balls in $2\times 2$ matrix, we give an interpretation of the multiplication $2\times 2$ of numbers, but as a number this arrangement equals to $4$: $$2\times2\ =\ 4 $$ Similarly, we might want that e.g. the Klein group $V_4$ and the product group $\Bbb Z_2\times\Bbb Z_2$ would be equal, as groups (independently of exactly which four elements build them and how). $$\Bbb Z_2\times\Bbb Z_2\ =\ V_4$$
As you have found, categories --as defined in HoTT-- are indeed necessarily skeletal in that setting.
That 'Skeletons violate the principle of equivalence' refers to the fact that the property 'skeletal' is not invariant under category equivalence.
As every category (in the sense and context of HoTT[!]) is skeletal, category equivalence here seems to coincide to category isomorphism, hence -by Univalence- to equality.
In HoTT the notion 'skeletal' just gets meaningless.
But the whole HoTT theory is still under development, terms and definitions are not necessarily in their finalized form yet..