Commit 2024-07-10 18:10 0d7d1283

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