Commit 2025-12-23 11:47 9c7dee5d

View on Github →

chore(CategoryTheory): deprecate cartesian closed categories API (#33228)

Estimated changes

Modified Mathlib/CategoryTheory/Category/Cat/CartesianClosed.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean

added def CategoryTheory.MonoidalClosed.unitIsoSelf

Modified Mathlib/CategoryTheory/Monoidal/Closed/Cartesian.lean

deleted def CategoryTheory.CartesianClosed.curry

deleted theorem CategoryTheory.CartesianClosed.curry_eq

deleted theorem CategoryTheory.CartesianClosed.curry_eq_iff

deleted theorem CategoryTheory.CartesianClosed.curry_id_eq_coev

deleted theorem CategoryTheory.CartesianClosed.curry_injective

deleted theorem CategoryTheory.CartesianClosed.curry_natural_left

deleted theorem CategoryTheory.CartesianClosed.curry_natural_right

deleted theorem CategoryTheory.CartesianClosed.curry_uncurry

deleted theorem CategoryTheory.CartesianClosed.eq_curry_iff

deleted theorem CategoryTheory.CartesianClosed.homEquiv_apply_eq

deleted theorem CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq

deleted def CategoryTheory.CartesianClosed.mk

deleted def CategoryTheory.CartesianClosed.uncurry

deleted theorem CategoryTheory.CartesianClosed.uncurry_curry

deleted theorem CategoryTheory.CartesianClosed.uncurry_eq

deleted theorem CategoryTheory.CartesianClosed.uncurry_id_eq_ev

deleted theorem CategoryTheory.CartesianClosed.uncurry_injective

deleted theorem CategoryTheory.CartesianClosed.uncurry_natural_left

deleted theorem CategoryTheory.CartesianClosed.uncurry_natural_right

deleted def CategoryTheory.binaryProductExponentiable

deleted theorem CategoryTheory.coev_app_comp_pre_app

deleted theorem CategoryTheory.exp.coev_ev

deleted theorem CategoryTheory.exp.ev_coev

deleted def CategoryTheory.expUnitIsoSelf

deleted def CategoryTheory.expUnitNatIso

modified theorem CategoryTheory.initial_mono

deleted def CategoryTheory.internalHom

modified def CategoryTheory.internalizeHom

modified def CategoryTheory.powZero

deleted def CategoryTheory.pre

deleted theorem CategoryTheory.pre_id

deleted theorem CategoryTheory.pre_map

deleted theorem CategoryTheory.prod_map_pre_app_comp_ev

deleted def CategoryTheory.terminalExponentiable

deleted theorem CategoryTheory.uncurry_pre

Modified Mathlib/CategoryTheory/Monoidal/Closed/Functor.lean

modified def CategoryTheory.expComparison

Modified Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean

modified def CategoryTheory.cartesianClosedOfReflective

Modified Mathlib/CategoryTheory/Monoidal/Closed/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Zero.lean

Modified Mathlib/CategoryTheory/Sites/CartesianClosed.lean

Modified Mathlib/Condensed/CartesianClosed.lean

Modified Mathlib/Condensed/Light/CartesianClosed.lean