Commit 2022-03-05 03:06 fdf43f1c

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.