Pullback consequences extensivity

Proof. A pullback square whose lower right corner is \(Y_i\) is equivalently a pullback square in the slice category \(C_{/Y_i}\). Under the equivalence \[ \prod _i C_{/Y_i} \longrightarrow C_{/\coprod _i Y_i} \] from Definition 13.3.1, a collection of such squares is sent to its coproduct. Since equivalences preserve pullbacks, this proves part (1).

For part (2), recall that a right adjoint to postcomposition between slice categories computes pullback along the relevant morphism. Under the equivalence \[ C_{/Y} \times C_{/Y} \longrightarrow C_{/Y \sqcup Y}, \] postcomposition with \(\nabla \colon Y \sqcup Y \to Y\) identifies with the coproduct functor \(C_{/Y} \times C_{/Y} \to C_{/Y}\). Its right adjoint is the diagonal functor, so pullback along \(\nabla \) sends \(r\) to \(r \sqcup r\). The counit square is precisely the first square in (13.2).

For the second square, the case \(n=0\) of Definition 13.3.1 says that \(C_{/\emptyset }\) is terminal. Postcomposition along \(\emptyset \to Y\) selects the initial object \(\emptyset \to Y\) of \(C_{/Y}\) and is therefore left adjoint to the unique functor \(C_{/Y} \to C_{/\emptyset }\). Thus pullback along \(\emptyset \to Y\) sends \(r\) to the unique object of \(C_{/\emptyset }\), and its counit square is the second square in (13.2). □