mathlib3

fdf43f1c - feat(category_theory/closed): generalize some material from cartesian closed categories to closed monoidal categories (#12386)

feat(category_theory/closed): generalize some material from cartesian closed categories to closed monoidal categories (#12386) No new content, just moving some trivially generalisable material about cartesian closed categories to closed monoidal categories. I've defined `ihom` for internal hom, and made `exp` an abbreviation for it in the cartesian closed case. A few other definitions similarly become abbreviations. I've left the `⟹` arrow for the internal hom in the cartesian closed case, and added `⟶[C]` for the general internal hom. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>