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

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!

• CAn you please tell me what the HoTT book is ? – Rene Schipperus Sep 17 '14 at 14:07
• The Homotopy Type Theory book. You can google it and download it for free. – Jovana Sep 17 '14 at 14:09
• Why would you want to define a (pre)category inside a 2-category? The point of a 2-category is that its objects are already category-like. – Zhen Lin Sep 17 '14 at 15:01
• I am learning about the formalisation of category theory inside the homotopy type theory, so everything I am trying to do is in univalent foundations. Maybe I don't need to define a precategory inside a 2-category! The question is how much of the formalised (ordinary) category theory can be done internaly to an arbitrary 2-category. What does this question precisely mean? – Jovana Sep 17 '14 at 15:40
• That's almost surely a joke exercise, along the same lines as Lang's famous "Take any book on homological algebra, and prove all the theorems without looking at the proofs given in that book." – Zhen Lin Sep 17 '14 at 16:03

## 1 Answer

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.