I agree that doing category theory without homotopy type theory is working with one hand tied behind your back, but you have to realize that it is very differen

I agree that doing category theory without homotopy type theory is working with one hand tied behind your back, but you have to realize that it is very different from textbook category theory. For instance, in HoTT you will find that the category of U-small categories is not a 1 category; it's a 2 category (since equality of categories is equivalence, not isomorphism). This is correct and gets rid of a lot of confusion surrounding Cat, but it means that you have to deviate from the textbook definitions a lot. There are at least two formalization of HoTT categories if anybody wants to know more. There's one formalization in HoTT Coq and the formalization as part of the unimath project. Both work heavily with precategories as well as categories in order to formulate some textbook notions without changing all the definitions...