Def CategoryTheory.cartesianClosedOfReflective'

Modification history

2025-10-01 17:16
Mathlib/CategoryTheory/Closed/Ideal.lean
feat(CategoryTheory/Closed): variant of `cartesianClosedOfReflective` with better definitional equalities (#30017) …
Added CategoryTheory.cartesianClosedOfReflective'View on Github →