Switch the arguments of (Co)ClosedMonoidalLeft/RightCoevaluationMorphism

[mohamed-barakat]

For the legacy CAP operations of the parametric adjunction $-\otimes a \dashv \mathrm{\underline{Hom}}(a,-)$

• EvaluationMorphism($a,b$) is the adjunction counit $(\varepsilon_a)_b: \mathrm{\underline{Hom}}(a,b) \otimes a \rightarrow b$,
• CoevaluationMorphism($b,a$) is the adjunction unit $(\eta_a)_b: b \rightarrow \mathrm{\underline{Hom}}(a, b \otimes a)$.

(note: in the documentation of CoevaluationMorphism $a$ and $b$ are permuted)

Contra-intuitively, the first argument $b$ of CoevaluationMorphism is the component while the second is the parameter $a$ of the parametric adjunction. In any case, the orders of the arguments for the unit and the counit are incompatible.

Now that we have the new names ClosedMonoidalLeftEvaluationMorphism etc., I would like to fix this mismatch. If desired I could also change CoevaluationMorphism from currently being a (backward compatibility) synonym of ClosedMonoidalLeftEvaluationMorphism to an operation exhibiting the old flipped order of arguments.

[mohamed-barakat]

If there are no objections the next PR will address this issue.