Commit 2022-05-02 11:44 a6275694

feat(category_theory/monoidal): adjunctions in rigid categories (#13707) We construct the bijection on hom-sets (Yᘁ ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z) given by "pulling the string on the left" down or up, using right duals in a right rigid category. As consequences, we show that a left rigid category is monoidal closed (it seems our lefts and rights have got mixed up!!), and that functors from a groupoid to a rigid category is again a rigid category.