Zulip Chat Archive
Stream: general
Topic: Discrete monoidal categories
Yaël Dillies (Jul 15 2022 at 14:22):
Aren't docs#discrete.add_monoidal and docs#category_theory.discrete.monoidal creating a diamond when M is a ring? Should we have add_discrete and mul_discrete instead of just discrete?
Yaël Dillies (Jul 15 2022 at 14:37):
It sounds like a remake of the docs#opposite, docs#mul_opposite, docs#add_opposite story.
Last updated: Dec 20 2023 at 11:08 UTC