Commit 2020-04-20 11:18 44743821

feat(category_theory/opposites): some opposite category properties (#2464) Add some more basic properties relating to the opposite category. Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant For reviewers: code review check list If you're confused by comments on your PR like bors r+ or bors d+, please see our notes on bors for information on our merging workflow.