CatDat

Implication Details

Claim: If a category is cocomplete and is extensive and is locally cartesian closed, then it is infinitary extensive.

Proof: The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the nLab.

Show 2 categories using this implication