<p>I refer you to <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA303#v=onepage&amp;q&amp;f=false">Chapter 9</a> of the HoTT book. In particular, a <em>category</em> is defined in such a way that isomorphic objects are equal, see <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA305#v=onepage&amp;q&amp;f=false">Definition 9.1.6</a>. As <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA306#v=onepage&amp;q&amp;f=false">Example 9.1.15</a> 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".</p>

<p>Furthermore, <a href="http://books.google.si/books?id=LkDUKMv3yp0C&amp;lpg=PP1&amp;pg=PA317#v=onepage&amp;q&amp;f=false">Theorem 9.4.16</a> says</p>

<blockquote>
  <p><strong>Theorem 9.4.16:</strong> <em>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.</em></p>
</blockquote>

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

<p>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.</p>

CC BY-SA 3.0
2014-11-02T19:44:29.907Z
2014-11-02T19:51:36.753Z
2014-11-02T19:51:36.753Z
Andrej Bauer
<p>Say I work in <a href="http://en.wikipedia.org/wiki/Homotopy_type_theory">homotopy type theory</a> and my sole objects of study are conventional categories. </p>

<p>Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and  $G:{\bf C}\longrightarrow{\bf D}$ which provide <a href="http://en.wikipedia.org/wiki/Equivalence_of_categories">equivalences of categories</a> ${\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.</p>

<p>Now <a href="http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence_axiom">univalence</a> 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 <a href="http://en.wikipedia.org/wiki/Skeleton_%28category_theory%29">skeletons</a>, I wonder if I can express the univalence axiom in terms of passing to the skeleton of the categories. </p>

<p>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."?</p>

<p>(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 <a href="http://ncatlab.org/nlab/show/principle+of+equivalence">principle of equivalence</a>, which is already a natural part of the formulation of category theoretical statements, e.g. specifying objects only in terms universal properties.)</p>

CC BY-SA 3.0
2014-11-02T19:32:56.493Z
Have you read Chapter 9 of the HoTT book? It's about category theory.
Andrej Bauer
<type-theory><ct.category-theory><dependent-type><equivalence><homotopy-type-theory>
Relating univalence for a theory of cateogries to the skeleton concept
Nikolaj-K
# Relating univalence for a theory of cateogries to the skeleton concept

(Asked by: username_0 on 2014-10-30)

Say I work in [homotopy type theory](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Equivalence_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](http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence_axiom) 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](http://en.wikipedia.org/wiki/Skeleton_%28category_theory%29), 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](http://ncatlab.org/nlab/show/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.)

**Tags:** type-theory, ct.category-theory, dependent-type, equivalence, homotopy-type-theory

> **Comments:**
> **username_1**: Have you read Chapter 9 of the HoTT book? It's about category theory.  

---

## 1 answers

### Answer by username_1 on 2014-11-02. Score: 11 | Accepted answer

I refer you to [Chapter 9](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA303#v=onepage&q&f=false) of the HoTT book. In particular, a *category* is defined in such a way that isomorphic objects are equal, see [Definition 9.1.6](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA305#v=onepage&q&f=false). As [Example 9.1.15](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA306#v=onepage&q&f=false) 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](http://books.google.si/books?id=LkDUKMv3yp0C&lpg=PP1&pg=PA317#v=onepage&q&f=false) 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.


---

