make discrete a structure #13762

Stream: PR reviews

[Scott Morrison]

This is a boring PR about making discrete in the category theory library a structure. It touches lots of files, so may rot.

However I think it's a helpful fix: my previous efforts to clean up the has_shift API, in turn motivated by trying to bring bounded and derived categories over from LTE, all foundered on discrete leaking through the confusing ways. So I hope this boring fix will enable good things.

[Scott Morrison]

It is not a perfect PR. There is quite a bit of annoyance around having categorical products being indexed by discrete walking_pair now; lots of extra brackets and .as. I just focussed in this PR on making everything work again after making discrete a structure, and did not consider refactoring the categorical product API itself.

[Scott Morrison]

If anyone would like to discuss such a refactor, do it themselves, or pressure me to think about, that's all fine. But I'm hoping that it doesn't need to prevent this PR being merged. :-)