Terminology: `IsDistributiveCategory` vs. `IsDistributiveBicartesianCategory`

[zickgraf]

I have seen on nLab that IsDistributiveCategory is standard terminology for a bicartesian category with a distributivity law for products and coproducts. I would still suggest to call it IsDistributiveBicartesianCategory in CAP to avoid confusion ~, especially if we later introduce IsDistributiveMonoidalCategory. Otherwise it would be very easy to confuse IsMonoidalCategory and IsDistributiveCategory and IsDistributiveMonoidalCategory, i.e. assume an implication in at least one direction~.

[mohamed-barakat]

I have seen on nLab that IsDistributiveCategory is standard terminology for a bicartesian category with a distributivity law for products and coproducts. I would still suggest to call it IsDistributiveBicartesianCategory in CAP to avoid confusion, especially if we later introduce IsDistributiveMonoidalCategory. Otherwise it would be very easy to confuse IsMonoidalCategory and IsDistributiveCategory and IsDistributiveMonoidalCategory, i.e. assume an implication in at least one direction.

IsDistributiveMonoidalCategory only makes sense if we know over what the tensor product distributes. In case of the direct sum we already call it "additive monoidal categories". However, we did not introduce the corresponding and-filter.

[zickgraf]

IsDistributiveMonoidalCategory only makes sense if we know over what the tensor product distributes.

nLab says: "A distributive monoidal category is a monoidal category whose tensor product distributes over coproducts." But indeed it also mentions that "this is not entirely standard terminology".

In case of the direct sum we already call it "additive monoidal categories". However, we did not introduce the corresponding and-filter.

Which and-filter do you mean?

[mohamed-barakat]

In case of the direct sum we already call it "additive monoidal categories". However, we did not introduce the corresponding and-filter.

Which and-filter do you mean?

IsAdditiveMonoidalCategory. I believe we did not introduce it since a monoidal structure on an additive category does not necessarily distribute over the direct sum. E.g., the direct sum as a monoidal structure does not distribute over itself.

[mohamed-barakat]

The terminology IsDistributiveMonodialCategory on nLab is biased towards coproduct.

[zickgraf]

I still find IsDistributiveCategory confusing (independent of the existence and/or definition of IsDistributiveMonodialCategory) and would suggest naming it IsDistributiveBicartesianCategory. However, if you think IsDistributiveCategory is generally understood, feel free to close the issue.

[mohamed-barakat]

What about making IsDistributiveBicartesianCategory a synonym? We can wait until Julia supports DeclareSynonym.

[zickgraf]

Would IsDistributiveBicartesianCategory be a synonym of IsDistributiveCategory or the other way round? I.e. would Display( IsDistributiveBicartesianCategory ) print

<Property "IsDistributiveCategory">

or

<Property "IsDistributiveBicartesianCategory">

?

[mohamed-barakat]

Display( IsDistributiveBicartesianCategory ) would print IsDistributiveCategory.

[zickgraf]

Display( IsDistributiveBicartesianCategory ) would print IsDistributiveCategory.

I think this would be even more confusing :D I will close the issue.