This defines BddOrd, the category of bounded orders.
The category of bounded orders with monotone functions.
The underlying object in the category of partial orders.
Construct a bundled BddOrd from a Fintype PartialOrder.
OrderDual as a functor.
Constructs an equivalence between bounded orders from an order isomorphism between them.
The equivalence between BddOrd and itself induced by OrderDual both ways.