Jacopo Emmenegger: A glimpse of pretoposes

I will give a brief introduction to the basic categorical structures considered in categorical logic, namely coherent categories, and focus then on a subclass of them. These particular categories are called pretoposes and can be characterized, among coherent categories, from a purely logical point of view. The first half of this characterization is given by a property known as conceptual completeness, and the other half by a construction called pretopos completion. I will explain what these two amount to and, hopefully, briefly describe the construction of the latter.