Internal categories as models of homotopy types

A homotopy n-type is a topological space which has trivial homotopy groups above degree n. Every space can be constructed from a sequence of such homotopy types, in a sense made precise by the theory of Postnikov towers, yielding improving `approximations' to the space by encoding information about the first n homotopy groups for increasing n. Thus the study of homotopy types, and the search for models of such spaces that can be fruitfully investigated, has been a central problem in homotopy theory. Of course, a homotopy 0-type is, up to weak homotopy equivalence (isomorphism of homotopy groups), a discrete set. It is well-known that a connected 1-type can be represented, again up to weak homotopy equivalence, as the classifying space of its fundamental group: this is the geometric realization of the simplicial set that is the nerve of the group regarded as a category with one object. Another way to phrase this is that the homotopy category of 1-types obtained by localizing at maps which are weak homotopy equivalences | formally adding inverses for these | is equivalent to the skeleton of the category of groups. In [Mac Lane and Whitehead] it was proved that connected homotopy 2-types can be modeled, in the sense described above, by crossed modules of groups. A crossed module is equivalently what in [Loday] is called a 1-cat-group, but now often referred to as a cat