untyped lambda calculus. The Karoubi envelope of an extensional lambda model (a monoid, considered as a category) is cartesian closed. The category of projective modules over any ring is the Karoubi envelope of its full subcategory of free modules. The category of vector bundles over any paracompact space is the Karoubi envelope of its full subcategory of trivial bundles. This is in fact a special case of the previous example by the Serre–Swan theorem and conversely this theorem can be proved by first proving both these facts, the observation that the global sections functor is an equivalence between trivial vector bundles over and free modules over and then using the universal property of the Karoubi envelope. References Category theory