# Relating univalence for a theory of cateogries to the skeleton concept

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

• Have you read Chapter 9 of the HoTT book? It's about category theory. – Andrej Bauer Nov 2 '14 at 19:32

Theorem 9.4.16: If $A$ and $B$ are categories then the function $$(A = B) \to (A \simeq B)$$ (defined by induction on the identity functor) is an equivalence of types.
You ask whether you can reduce the Univalence axiom to a statement about categories. Attempts using skeletons won't work because there isn't a good way to say "skeletal". We could ask whether Theorem 9.4.16 implies the Univalence axiom. This is not going to be the case, as far as I can see, because a category has a $1$-type (groupoid) of objects and a $0$-type (set) of morphisms, so theorem 9.4.16 amounts to something like the Univalence axiom for 1-types, only.