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

  • 2
    $\begingroup$ Have you read Chapter 9 of the HoTT book? It's about category theory. $\endgroup$ Nov 2, 2014 at 19:32

1 Answer 1


I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't a reasonable notion of "skeletality" in HoTT. This is so because equality is so weak that it already means "isomorphic".

Furthermore, Theorem 9.4.16 says

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.

The theorem tells us that the Univalence Axiom gives us a sort of cateory theorist's dream: equivalent categories are equal.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.