Commit 2022-03-05 03:06 fdf43f1cView on Github →
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.
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.