Implication Details
Claim: If a category has disjoint finite coproducts and is locally cartesian closed, then it is extensive.
Proof: The pullback functor preserves finite coproducts because it has a right adjoint. Remark: In combination with other implication, this result implies that every elementary topos is extensive.