Open HuStmpHrrr opened 2 years ago
I notice that the proof is inlined as part of the proof that a CCC is monoidal closed:
https://github.com/agda/agda-categories/blob/b4b2f80b473efaa99421f37a56c961d6da28ef82/src/Categories/Category/CartesianClosed.agda#L235
I think this proof is worth its own place, maybe as a property of CCC.
Good idea.
I notice that the proof is inlined as part of the proof that a CCC is monoidal closed:
https://github.com/agda/agda-categories/blob/b4b2f80b473efaa99421f37a56c961d6da28ef82/src/Categories/Category/CartesianClosed.agda#L235
I think this proof is worth its own place, maybe as a property of CCC.