unifying `order_dual` and `opposite`

Stream: general

[Scott Morrison]

I would really like to unify order_dual in order/basic.lean with opposite in category_theory/opposites.lean.

[Scott Morrison]

They are talking about exactly the same thing, and to do presheafs and sheafs nicely I think we'll want to reflect a lot of the order structure on open sets up in category theoretic language. On the category theory side we'll be talking about (opens X)\op, and it's very sad at the moment there isn't just a complete_lattice immediately available, precisely because order_dual and opposite are not identical.

[Scott Morrison]

@Mario Carneiro, @Reid Barton, @Johannes Hölzl, any ideas about how to proceed?

[Mario Carneiro]

That sounds difficult... You would have to have preorder be the same thing as category

[Scott Morrison]

Why is that?

[Scott Morrison]

I was just thinking to move the definition def opposite (C : Sort u₁) : Sort u₁ := C (but nothing else) way down the import tree, and then search and replace order_dual for opposite.

[Mario Carneiro]

You could equip opposite with a preorder separate from its category, although you then have a diamond

[Scott Morrison]

oh, I see, a diamond

[Scott Morrison]

there would be two ways to get category (opens X)\op

[Scott Morrison]

either make the opposite preorder, then build a category from that

[Scott Morrison]

or make the category from the preorder, and take the opposite category

[Scott Morrison]

... tedious

[Mario Carneiro]

if you are lucky it might be defeq

[Kevin Buzzard]

Rather bizarrely I was experimenting with this stuff on the way home from AITP yesterday -- I decided that I could try to prove that the categories built in these two ways were equivalent -- it certainly didn't occur to me to try and make them defeq :-)