Def CategoryTheory.expTerminalNatIso

Modification history

2024-11-14 20:44
Mathlib/CategoryTheory/Closed/Cartesian.lean
refactor: change `CartesianClosed` to rely on `ChosenFiniteProducts` (#17766) …
Deleted CategoryTheory.expTerminalNatIsoView on Github →
2024-09-26 00:42
Mathlib/CategoryTheory/Closed/Cartesian.lean
feat(CategoryTheory): the internal hom with the monoidal unit is the identity (#17065) …
Added CategoryTheory.expTerminalNatIsoView on Github →