adjoint functor theorem
adjoint lifting theorem
small object argument
Freyd-Mitchell embedding theorem
relation between type theory and category theory
sheaf and topos theory
enriched category theory
higher category theory
Edit this sidebar
A functor F:C→D between coherent categories is called coherent if it is a regular functor and in addition preserves finite unions.
For 𝒯 a coherent theory and 𝒞 𝕋 its syntactic category, coherent functors 𝒞 𝕋→ℰ into some topos ℰ are precisely models of the theory in ℰ.
For 𝒞 𝕋 equipped with the structure of the syntactic site (the coherent coverage), this is in turn equivalent to geometric morphisms ℰ→Sh(𝒞 𝕋) into the sheaf topos over 𝒞 𝕋 (the classifying topos for the theory).
Page 34 of