[Merged by Bors] - feat(CategoryTheory/Generator): introduce classes HasDetector and HasSeparator

[datokrat]

This change defines the typeclasses HasDetector and HasSeparator for categories with detectors/separators. Several results for IsDetector and IsSeparator are also proved for the new typeclasses.

Convenience theorems for proving the well-poweredness of categories with separators are added, too.

Two typos are fixed: "separating" is corrected to "coseparating" in the module docstring and IsCospearator.isCodetector is renamed to IsCoseparator.isCodetector.

---

[github-actions]

PR summary 7e958ef66e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ HasCodetector
+ HasCodetector.hasCoseparator
+ HasCodetector.hasDetector_of_hasCodetector_op
+ HasCodetector.hasDetector_op
+ HasCoseparator
+ HasCoseparator.hasCodetector
+ HasCoseparator.hasSeparator_of_hasCoseparator_op
+ HasCoseparator.hasSeparator_op
+ HasDetector
+ HasDetector.hasCodetector_of_hasDetector_op
+ HasDetector.hasCodetector_op
+ HasDetector.hasSeparator
+ HasDetector.wellPowered
+ HasSeparator
+ HasSeparator.hasCoseparator_of_hasSeparator_op
+ HasSeparator.hasCoseparator_op
+ HasSeparator.hasDetector
+ HasSeparator.wellPowered
+ IsCoseparator.isCodetector
+ codetector
+ coseparator
+ detector
+ hasCodetector_op_iff
+ hasCoseparator_op_iff
+ hasDetector_op_iff
+ hasSeparator_op_iff
+ isCodetector_codetector
+ isCodetector_coseparator
+ isCoseparator_codetector
+ isCoseparator_coseparator
+ isDetector_detector
+ isDetector_separator
+ isSeparator_detector
+ isSeparator_separator
+ separator
+ wellPowered_of_isSeparator
- IsCospearator.isCodetector

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[datokrat]

While wellPowered_of_isSeparator can be inlined quite trivially and might be unnecessary, I think HasSeparator.wellPowered can be actually useful. Happy to hear opinions on this :)

[datokrat]

While applying the suggestions, I decided to make C implicit in hasSeparator_op_iff etc.. This way, one does not need to supply the category in hasSeparator_op_iff.mp proof_hasSeparator_C_op. I'd be interested what you think about that!

[TwoFX]

Thanks!
bors d+

[mathlib-bors]

✌️ datokrat can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[datokrat]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style