search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Product functors are (braided/symmetric) monoidal #280

Closed sstucki closed 3 years ago

sstucki commented 3 years ago

... if they go between (braided/symmetric) monoidal categories.

sstucki commented 3 years ago

Yep it should be ready. I checked using make test locally, so I expect Travis to be happy too.

Yes, it's all boilerplate. It would be nice to avoid doing these things by hand. There seems to be a lot of boilerplate stuff for monoidal categories in general...

JacquesCarette commented 3 years ago

My guess is that this is true of many "lifting" operations, where properties in the base case lift across a nice operation. The same probably will happen from some unary functors too.