CatDat

Implication Details

Assumptions: disjoint finite coproductslocally cartesian closed

Conclusions: extensive

Reason: 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.