Proof of a conjecture of A. Pitts (Q1818641)

The subject of lax descent for several classes of morphisms has been extensively investigated by \textit{A. M. Pitts} in several lectures at conferences in Category Theory but are mostly unpublished. A well-known theorem of this kind [\textit{A. M. Pitts}, ``Lax descent for geometric morphisms'', Lecture, Cambridge Categories Conference, July 1986)] says that if the lower leg in a lax pullback of toposes over a base topos \({\mathcal S}\) is essential, then the geometric morphism opposite it is locally connected and moreover the Beck-Chevalley condition is satisfied. Its original proof is carried out by looking at the theories which the toposes in question classify so that, in this sense, it becomes a (definability) theorem in logic. A different proof of this result [\textit{M. Bunge} and \textit{J. Funk}, ``Spreads and the symmetric topos'', J. Pure Appl. Algebra 113, No. 1, 1-38 (1996; Zbl 0861.18004)] employs instead the topos classifying \({\mathcal S}\)-valued distributions on toposes bounded over \(\mathcal S\) and the explicit construction of the complete spread associated with an \(\mathcal S\)-valued distribution. The corresponding ``lax descent theorem'' for coherent toposes (actually, coherence morphisms in the relative version) was conjectured by Pitts who pointed out that the key result needed was the Beck-Chevalley condition. The dual version for pretoposes was proved by \textit{M. W. Zawadowski} [``Descent and duality'', Ann. Pure Appl. Logic 71, No. 2, 131-188 (1995; Zbl 0815.18003)] and interpreted as a definability result for coherent logic. A different, model-theoretic proof, was given later by \textit{D. Ballard} and \textit{W. Boshuk} [J. Symb. Log. 63, No. 2, 372-378 (1998; Zbl 0908.18001)]. The paper being reviewed provides yet another proof of this result which claims to be simpler than the already existing proofs. The proof relies basically on the Grothendieck construction of filtered inverse limits of toposes [\textit{M. Artin, A. Grothendieck} and \textit{J. L. Verdier}, SGA 4, Lect. Notes Math. 269 (1972; Zbl 0234.00007)] and of specific refinements in the case of coherent toposes (equivalently, of finitary sites).