CatDat

Implication Details

Assumptions: disjoint finite coproductsregular-quotient-trivial

Conclusions: trivial

Proof: For any object XX, the coequalizer of the two coprojections XXXX \rightrightarrows X \sqcup X is the codiagonal :XXX\nabla : X \sqcup X \to X. Therefore, these two coprojections are equal. But their equalizer is also the unique morphism !:0X! : 0 \to X. It follows that !:0X! : 0 \to X is an isomorphism.

Show 24 categories using this implication