Lexicographic order for sum. Sort all the inl a before the inr b, otherwise use the respective order on α or β.

Swap the factors of a sum type