Initial-object lemma for complete categories with a weakly initial set

ID: initial-object-lemma-for-complete-categories-with-a-weakly-initial-set

A locally small category with all small categorical limits and a small weakly initial set has an initial object. Take the product of the weakly initial family, then the simultaneous equalizer of all endomorphisms of and its identity. For any parallel , their equalizer receives a map . The equation forces , so is invertible and . Weak initiality supplies existence of maps from . This is the smallness mechanism in the Freyd general adjoint functor theorem.

New to topics? Read the docs here!