There are several categories for which the proofs for the negations of "counital" and "CIP" are the same (namely Grp.yaml, Mon.yaml, Rng.yaml, Set_pointed.yaml (dualized), Top_pointed.yaml (dualized)). This is because a property in between is missing, something that might be called "binary CIP". This shall mean that binary products, binary coproducts, and zero morphisms exist, and for all pairs of objects $X,Y$ the canonical morphism $X \sqcup Y \to X \times Y$ is a monomorphism.
Then we have the following implications:
- counital + binary products ==> binary CIP
- CIP ===> binary CIP
Then we only need to prove that a category (with binary products) does not satisfy "binary CIP" to disprove the other properties. The proof duplication is removed.
The dual property should also be added. A category satisfies "binary CSP" when it has binary products, binary coproducts, zero morphisms, and for all pairs of objects $X,Y$ the canonical morphism $X \sqcup Y \to X \times Y$ is an epimorphism.
Notice:
- biproducts ==> binary CIP
- biproducts ==> binary CSP
Probably also something like: binary CIP + binary CSP + balanced => biproducts (need to check)
There are several categories for which the proofs for the negations of "counital" and "CIP" are the same (namely$X,Y$ the canonical morphism $X \sqcup Y \to X \times Y$ is a monomorphism.
Grp.yaml,Mon.yaml,Rng.yaml,Set_pointed.yaml(dualized),Top_pointed.yaml(dualized)). This is because a property in between is missing, something that might be called "binary CIP". This shall mean that binary products, binary coproducts, and zero morphisms exist, and for all pairs of objectsThen we have the following implications:
Then we only need to prove that a category (with binary products) does not satisfy "binary CIP" to disprove the other properties. The proof duplication is removed.
The dual property should also be added. A category satisfies "binary CSP" when it has binary products, binary coproducts, zero morphisms, and for all pairs of objects$X,Y$ the canonical morphism $X \sqcup Y \to X \times Y$ is an epimorphism.
Notice:
Probably also something like: binary CIP + binary CSP + balanced => biproducts (need to check)