Inverting preorder for category instance

Stream: new members

[VayusElytra]

Hello,

Currently I am working with a functor that looks like this:

def ExampleFunctor (P : Type) [Preorder P] : P ⥤ Type where
  obj D := sorry
  map f := sorry

In this way I get a functor that maps x ≤ y to a morphism in type ExampleFunctor x ⟶ ExampleFunctor y. However I would like to have instead a map ExampleFunctor y ⟶ ExampleFunctor x.

To do this I have of course tried writing a functor into the opposite category Typeᵒᵖ, but this was a real nightmare. I could also redefine my x ≤ y relation to be the other way around, but this would force me to rewrite a lot of unrelated proofs.

Is there a simple way to force Lean to use the ≥ relationship instead to obtain the category structure on P, so that I do not need to invert any arrows?

[Adam Topaz]

You can use docs#OrderDual (with the od notation similar to op) to reverse the order relation

[VayusElytra]

Thank you, this is perfect.