Commit 2022-03-12 14:08 a63b99c3

View on Github →

chore(category_theory/closed/monoidal): fix notation (#12612) Previously the C in the internal hom arrow ⟶[C] was hardcoded, which wasn't very useful! I've also reduced the precedence slightly, so we now require more parentheses, but I think these are less confusing rather than more so it is a good side effect?

Estimated changes

Modified src/category_theory/closed/monoidal.lean

modified def category_theory.monoidal_closed.curry

modified theorem category_theory.monoidal_closed.curry_eq_iff

modified theorem category_theory.monoidal_closed.curry_injective

modified theorem category_theory.monoidal_closed.curry_uncurry

modified theorem category_theory.monoidal_closed.eq_curry_iff

modified theorem category_theory.monoidal_closed.hom_equiv_symm_apply_eq

modified def category_theory.monoidal_closed.uncurry

modified theorem category_theory.monoidal_closed.uncurry_eq

modified theorem category_theory.monoidal_closed.uncurry_injective

modified theorem category_theory.monoidal_closed.uncurry_natural_left

modified theorem category_theory.monoidal_closed.uncurry_natural_right