Say I work in homotopy type theory and my sole objects of study are conventional categories. Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and  $G:{\bf C}\longrightarrow{\bf D}$ which provide equivalences of categories ${\bf C} \simeq {\bf D}$. There exist natural isomorphisms $\alpha:\mathrm{nat}(FG,1_{\bf C})$ and $\beta:\mathrm{nat}(GF,1_{\bf D})$ so that this functor and inverse functor are transformed to unit functor.Now univalence relates equivalences to the identity type ${\bf C}={\bf D}$ of the intentional type theory I have chosen to talk about categories. Since I only deal with categories and those are equivalent if they have isomorphic skeletons, I wonder if I can express the univalence axiom in terms of passing to the skeleton of the categories. Or, otherwise, can I define the identity type, i.e. the syntactic expression ${\bf C}={\bf D}:=\dots$in a way which essentially says there is a skeleton (or isomorphi) and ${\bf C}$ and ${\bf D}$ are both equivalent to it.?(In the above I try to interpret the type theory in terms of concepts which are easier to define - the category theoretical notions. I think about this because morally, it seems to me that the axiom corrects intentional type theory by hard-coding the principle of equivalence, which is already a natural part of the formulation of category theoretical statements, e.g. specifying objects only in terms universal properties.)
Relating univalence for a theory of cateogries to the skeleton concept
type theory;ct.category theory;dependent type;equivalence;homotopy type theory