Commit 2022-02-02 08:53 a6d70aa7

feat(order/category/*): order_dual as an equivalence of categories (#11743) For whatever a category of orders, define

• whatever.iso_of_order_iso: Turns an order isomorphism into an equivalence of objects inside whatever
• whatever.to_dual: order_dual as a functor from whatever to itself
• whatever.dual_equiv: The equivalence of categories between whatever and itself induced by order_dual both ways
• order_iso.dual_dual: The order isomorphism between α and order_dual (order_dual α)