demote priority of cocartesian monoidal structure

[Alizter]

The cocartesian monoidal structure for any wild category with coproducts had the same priority with the cartesian monoidal structure for any wild category with products. This meant that in practice, inferring a monoidal structure on say Type chose the cocartesian monoidal structure. This is due to the second instance appearing at the same priority but later.

This PR demotes the priority of the cocartesian monoidal structure so that the cartesian monoidal structure is generally preferred. The cocartesian monoidal structure is not used nearly as much in practice anyway.