CatDat

Implication Details

Assumptions: Grothendieck topos

Conclusions: cogeneratorinfinitary extensivelocally presentable

Reason: A Grothendieck topos is locally presentable by Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3, has a cogenerator (see nLab) and is infinitary extensive by Giraud's Theorem.