Choose hom(B,C) = C ⊗ B^v instead of B^v ⊗ C

[zickgraf]

Currently, CAP derives the closed structure from the rigid structure by setting hom(B,C) = B^v ⊗ C. nLab chooses hom(B,C) = C ⊗ B^v instead: https://ncatlab.org/nlab/show/compact+closed+category. This PR implement the nLab convention. This greatly simplifies the definition of the evaluation and coevaluation morphisms, which can now be defined without braidings. This in turn simplifies string diagrams and the proof that we indeed get a closed structure. On the other hand, some braidings have to be added at other places. However, those are maybe expected or could be avoided. For example, a derivation of the trace map now needs a braiding, but that already seems to be part of the definition: https://ncatlab.org/nlab/show/trace. Moreover, some derivations using TensorProductInternalHomCompatibilityMorphism now need a braiding, but maybe TensorProductInternalHomCompatibilityMorphism could be adjusted, too to avoid this.

For my applications, choosing hom(B,C) = C ⊗ B^v is much simpler, so I will use this in my thesis. Maybe that would also make sense for CAP in general?

ping @mohamed-barakat @sebastianpos @TKuh

[sebastianpos]

Good point. If we assume that we have no braiding in a monoidal category, then we have to be careful with directions. Here are the details:

• CAP provides an interface for left duals
• CAP provides an interface for right internal homs

By left duals, I mean the following convention:
$$\mathrm{evaluation}: A^{\ast} \otimes A \rightarrow 1$$
and
$$\mathrm{coevaluation}: 1 \rightarrow A \otimes A^{\ast}$$
From left duals you can build

• a right adjoint of $(- \otimes A)$, i.e., a right internal hom, by $(- \otimes A^{\ast})$
• a left adjoint of $(A \otimes -)$, i.e., a left internal cohom, by $(A^{\ast} \otimes -)$

but you cannot build the other 2 missing combinations. In particular, setting the right internal hom as you suggest is the natural choice.

[zickgraf]

Thanks for the analysis and confirmation @sebastianpos! I will talk to @mohamed-barakat about how we shall proceed.