Commit 2024-09-26 00:42 3488c1c2

feat(CategoryTheory): the internal hom with the monoidal unit is the identity (#17065) In a closed monoidal category, the internal hom defined by mapping out of the monoidal unit is naturally isomorphic to the identity. This specializes to an analogous result about exponentiating with the terminal object in a cartesian closed category.