This is a housekeeping PR. It touches a lot of code but the changes are mostly superficial: avoiding duplicate definitions of the same shorthands that appear over and over again, making notation more uniform, removing some duplication code/lemmas related to isos and making it easier to work both with isos and normal morphisms at the same time (see e.g. how the new Commutationᵢ module is used in Category.Monoidal.Properties).
… for working with isos and monoidal categories.
This is a housekeeping PR. It touches a lot of code but the changes are mostly superficial: avoiding duplicate definitions of the same shorthands that appear over and over again, making notation more uniform, removing some duplication code/lemmas related to isos and making it easier to work both with isos and normal morphisms at the same time (see e.g. how the new
Commutationᵢmodule is used inCategory.Monoidal.Properties).This also addresses some instances of #299.