Commit 2020-06-17 03:12 e40de30a

View on Github →

chore(category_theory/closed): move one thing to monoidal closed and fix naming (#3090) Move one of the CCC defs to MCC as an example, and make the naming consistent.

Estimated changes

Modified src/category_theory/closed/cartesian.lean

added def category_theory.cartesian_closed.curry

added def category_theory.cartesian_closed.uncurry

deleted def category_theory.is_cartesian_closed.curry

deleted def category_theory.is_cartesian_closed.uncurry

modified def category_theory.terminal_exponentiable

Modified src/category_theory/closed/monoidal.lean

added def category_theory.unit_closed

Modified src/category_theory/monoidal/category.lean