Def CategoryTheory.MonoidalClosed.unitNatIso

Modification history

2024-09-26 00:42
Mathlib/CategoryTheory/Closed/Monoidal.lean
feat(CategoryTheory): the internal hom with the monoidal unit is the identity (#17065) …
Added CategoryTheory.MonoidalClosed.unitNatIsoView on Github →