Jake-Gillberg
commented
4 years ago Hey, thanks so much for your comments on the draft pull requests.
it would probably be nice to add this as a separate definition and then redefine binary product in term of the vector one. This would imply that we don't have to update all the code which is currently using a product category
Yeah, this makes sense. I'm playing fast and loose with this right now trying to see if this form of productCategory fixes any of the current issues with Monoidal Categories.
I guess that defining products using vectors is still biased as right associative (to be explicit, they associate like (a, (b, c))), so we'd still need to provide an isomorphism to the left associative equivalent. Something like product [cat1, cat2, cat3] ~ (product (product cat1 cat2) cat3).
Yeah, I think I see your point here. Right now my abstraction is a bit leaky, but I was hoping that the Vect (and associated tuples) stayed internal to the representation of the product category and we would avoid needing something like this.
hi @Jake-Gillberg
this looks nice!
Just two observations:
it would probably be nice to add this as a separate definition and then redefine binary product in term of the vector one. This would imply that we don't have to update all the code which is currently using a product category
I guess that defining products using vectors is still biased as right associative (to be explicit, they associate like
(a, (b, c))), so we'd still need to provide an isomorphism to the left associative equivalent. Something likeproduct [cat1, cat2, cat3] ~ (product (product cat1 cat2) cat3).