A proof of a conjecture of A. Pitts

Abstract

In this paper we prove a conjecture of Andrew Pitts which states that the BeckChevalley condition holds for lax pullbacks or comma squares of coherent toposes see Theorem below Pitts conjecture was put forward as a way towards the lax descent theorem for coherent toposes Theorem below The latter entails a dual version for pretoposes which was eventually established by Zawadowski in the setting of Makkais elaborate theory of Stone duality Our results therefore furnish a proof of the lax descent theorem for pretoposes along the lines originally conceived by Pitts As explained in Zawadowskis paper this theorem can be interpreted as a very general denability result for coherent logic