Add isomorphisms of categories

[ScriptRaccoon]

This PR adds

• isomorphisms of categories (as a functor property)
• three new functors:
  • opposite monoid functor (an example of an isomorphism)
  • opposite category functor (an example of an isomorphism)
  • the equivalence between the trivial category and the walking isomorphism (the simplest example of an equivalence of categories which is not an isomorphism)