feat (Category Theory): redefine and extend mates (#13840)

The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more direct way: using pasting composition on 2-cells. 

This pull request:
(i) proposes a new definition of `Mates` to replace and rename the existing `transferNatTrans`
(ii) proposes a new definition of `Conjugates` to replace and rename the existing `transferNatTransSelf`
(iii) proves that the mates correspondence commutes with horizontal and vertical composition of squares, as well as some coherences relating mates to conjugates
(iv) updates the files that depends on this, involving two new proofs about exponentiation in cartesian closed categories