Full Subcategory: Ho(Grpd) ⊊ Ho(Cat)

Ho(Grpd) is a full subcategory of Ho(Cat). When any two categories of Ho(Cat) are groupoids in Ho(Grpd), all natural isomorphism classes of functors between them are natural isomorphism classes of functors in Ho(Grpd) too. Put another way, Ho(Grpd) has only some of the objects of Ho(Cat), but all of the arrows.

In terms of stuff, structure, and properties, groupoids are like categories but with extra properties.

full_subcategories: Ho(Grpd), Ho(Cat)

This data as json