Ho(Cat) is a name for the homotopy category of Cat. That is, is the category
This is an instance of a general construction which, given a 2-category, or more generally an n-category, produces a 1-category with the same objects and whose morphisms are equivalence classes of 1-morphisms in the original -category. Sometimes this is called the 1-truncation and denoted .
It can also be viewed as an in…
