Rels is also a symmetric monoidal category with Set's cartesian product

agda / agda-categories

A new Categories library for Agda

https://agda.github.io/agda-categories

MIT License

362 stars 68 forks source link

Rels is also a symmetric monoidal category with Set's cartesian product #356

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

You're right, it is all horribly strict. I think I can see how to make an unstrict version of Rels but I don't know how much work it'll be. I'll give it a go when I get some free time