Opposite category

Stream: general

[Yaël Dillies]

Is it on purpose that docs#category_theory.category.opposite is not called category_theory.opposite.category or opposite.category. I just had quite a hard time finding it.

[Reid Barton]

It's an instance so the name should not matter.

[Yaël Dillies]

Sure, but we still have a naming convention for instances.

[Eric Wieser]

Maybe it works for dot notation that way?

[Reid Barton]

It does seem a bit non-uniform--what would be the automatically assigned name?

[Yaël Dillies]

I doubt it. The category argument is an instance.

[Yaël Dillies]

It would be opposite.category_theory.category

[Reid Barton]

I guess category_theory.opposite.category seems best

[Yaël Dillies]

I would also be happy with opposite.category. I mostly care about the object bit coming before the instance bit, as is done everywhere else.

[Reid Barton]

Apparently I chose the current name 3+ years ago so I hereby give you blessing to change it!