(Theorem 8.1), but which I would hardly have taken the trouble to figure out without the
prodding of an application.
I have made an effort to make the paper reasonably self-contained. The necessary
background for reading the paper consists of basic notions of category theory (as can be found
in [CWM]), and the connections established between first order logic and pretoposes in [M/R].
The references [B/J] and [M3] may also be consulted for the latter. 2-categories are mentioned
in some abstract formulations, but in fact, only some very "concrete" 2-categories are actually
used. The reference [M/Pa] contains a certain amount of 2-category theory, tailored for needs
related to logic, certainly sufficient for the present purposes. At some points, technical matters
from [Ml] and [M2] are used.
The set-theoretic foundations adopted are those using Grothendieck universes (see
[SGA4]), also explained in section 1.1 of [M/Pa], except that what were written IL , LL , U~
there are called #Q , It. , Uy now.
The numbering of items such as definitions and lemmas starts from the beginning in
each section; when an item is referred to in another section, the number of the item's section is
prefixed to the item number.
I express my thanks to Marek Zawadowski for many fruitful conversations, and for his
decisive insights in the subject at hand. I also thank George Janelidze, Bill Boshuck and the
referee for their valuable remarks, which have contributed to improvements of the presentation.