Generalising canonical extension to the categorical setting (Q714727)

The paper presents a generalization to the setting of coherent categories of the existing notion of canonical extension for distributive lattices. The generalization is shown to satisfy a natural analogue of the universal property enjoyed by ordinary canonical extensions, and to restrict to the context of Heyting categories. Moreover, and most importantly from the perspective of topos theory, the main construction leads to an alternative description of the topos of types associated to a coherent theory (introduced by M. Makkai in 1981), shedding new light on its relationship with the classifying topos. Specifically, the topos of types associated to a coherent category \(\mathcal C\) is realized as the topos of sheaves on an internal locale (built from the subobject lattices in \(\mathcal C\)) in the topos of presheaves \([{\mathcal C}^{\mathrm{op}}, \mathbf{Set}]\) on \(\mathcal C\), and for any coherent theory \(\mathbb T\) and small full subcategory \(\mathcal K\) of the category of set-based models of \(\mathbb T\) satisfying appropriate conditions, the topos of types associated to \(\mathbb T\) is shown to be equivalent to the topos arising in the hyperconnected localic factorization of the canonical geometric morphism from \([{\mathcal K}, \mathbf{Set}]\) to the classifying topos of \(\mathbb T\). The paper is nicely written and we recommended its reading to anyone interested in the theory of canonical extensions and categorical logic.