2-category in HoTT: chapter 9 from the HoTT book

Question

After reading Awodey's book, and the HoTT book (and numerous other entries on these topics), I am (ambitiously) trying to do the exercises after the category theory chapter.

This concernes the exercise 9.5.

So, this is something I have done:

• In 9.4 I defined a pre-2-category $A$ to consist of the type $A_0$ of objects, such that for all $a,b:A$ the type $hom_{A}(a,b)$ forms a precategory.

• Now, for the definition of 2-category $A$ from 9.5 I require, for all $a,b:A$ that the $idtoiso_{a,b}$ be an equivalence, and that the type $hom_{A}(a,b)$ be a category. (Is this ok?)

• So, the question is how much of chapter 9 can be done internaly to an arbitrary 2-category. This is the point I am not sure how to start. I have read some articles on this, but of course coming from category theory only.

  My question is how to define a precategory within an arbitrary 2-category $A.$ Should I do the same as it is done in higher category theory, i.e. take two elements $a_0$ and $a_1$ of the type $A_0$ to be the "element of objects" and the "element of arrows", together with four $1$-arrows from $A$, which will represent identity, domain, codomain, and composition? But then, how should I impose the condition that composition is defined on the pullback $a_1 \times_{a_0}a_1$? Since this does not make sense in an arbitrary 2-category, I was thinking about defining a precategory by taking the type $hom_{A}(a,b)$ to be the type of objects....

Can you, please help me with this issue? This question sounds so naive, but after doing some research, it seems to me that I should read a book on higher category theory before trying to give an answer to it. If that is the case, can you please give me some nice reference, and some guidlines for answering this question.

Thank you!

Answer 1

As Zhen said, the question doesn't mean to define categories inside a 2-category, but to replace "categories" throughout the chapter by the objects of some 2-category. In other words, do "formal category theory" inside a 2-category, the way 2-categories are often used in mathematics.