Sets is not self-dual

[mmcqd]

Description

This PR contains a proof that Sets is not self-dual, which is placed in the new Cat/Instances/Sets/Counterxamples/ folder. To use in this proof, it also defines strict initial objects, proves Sets ^op is a category, and fixes a typo.

This is my first contribution so I expect my prose/code may need some improvement, I'm open to any criticism!

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs.
• All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[plt-amy]

Thank you!