I've been doing a bit of work extending the category theory base to include cartesian closed categories. This pull request adds the basic components for products and exponentials and instantiates them for Fun. I'm not 100% sure about how the global vs. local typeclass instances for products interacts with the way I've specified the typeclasses for curry and apply. I also imagine that there are more standard lemmas about CCC's that could be added to CategoryFacts.v, but I'm not sure where to look for a relevant list of lemmas, but this is a starting point.
Lysxia
commented
3 years ago
I've been doing a bit of work extending the category theory base to include cartesian closed categories. This pull request adds the basic components for products and exponentials and instantiates them for
Fun. I'm not 100% sure about how the global vs. local typeclass instances for products interacts with the way I've specified the typeclasses for curry and apply. I also imagine that there are more standard lemmas about CCC's that could be added toCategoryFacts.v, but I'm not sure where to look for a relevant list of lemmas, but this is a starting point.