Commit 2025-10-01 17:16 12fc3dac
View on Github →feat(CategoryTheory/Closed): variant of cartesianClosedOfReflective with better definitional equalities (#30017)
A variant of cartesianClosedOfReflective that allows for better control over the resulting exponentials. The main application of this is that exponentials of sheaves are now computed as exponentials of presheaves up to definitional equality.