Let \(C\) be a category with pullbacks such that groupoid colimits are universal in \(C\) (e.g. \(C\) is a topos). Consider a commutative diagram in \(C\) as follows:
Assume that the map \(Y'' \to Y'\) is an effective epimorphism. If both the left-hand square and the outer rectangle are pullback squares, then so is the right-hand square.
Proof
We need to show that the map \(X'\to X \times_Y Y'\) is an isomorphism. By the previous lemma, this may be tested after pullback along the effective epimorphism \(Y'' \twoheadrightarrow Y'\). The claim now follows by applying the 2-out-of-3 property to the following commutative diagram:
