When starting this project, I found it easier to not deal with these implementations, since the definitions involve a lot of bureaucracy. But it would probably be good to ultimately use these definitions (and thereby utilize all the theorems about them). So perhaps the existing definition could be some kind of interface for easily producing mathlib's notions of finite product categories and cartesian closed categories.
The mathlib has defined these notions, e.g.
When starting this project, I found it easier to not deal with these implementations, since the definitions involve a lot of bureaucracy. But it would probably be good to ultimately use these definitions (and thereby utilize all the theorems about them). So perhaps the existing definition could be some kind of interface for easily producing mathlib's notions of finite product categories and cartesian closed categories.