Core of a Category

The core of a category 𝒞 𝒞 \mathcal{C} , denoted Core ⁢ ( 𝒞 ) Core 𝒞 \mathrm{Core}(\mathcal{C}) , is the Wide Subcategory of 𝒞 𝒞 \mathcal{C} formed by restricting to only the Isomorphisms.

This construction extends to a Pseudofunctor Core : Cat → Grpd : Core → Cat Grpd \mathrm{Core}:\mathrm{Cat}\to\mathrm{Grpd} ; moreover, this has a nice universal property: it is Right Biadjoint to the inclusion forgetful Pseudofunctor U : Grpd → Cat : 𝑈 → Grpd Cat U:\mathrm{Grpd}\to\mathrm{Cat} .