Finite intervals in a disjoint union #
This file provides the
LocallyFiniteOrder instance for the disjoint sum of two orders.
Do the same for the lexicographic sum of orders.
α₁ → β₁ → Finset γ₁ and
α₂ → β₂ → Finset γ₂ to a map
α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂). Could be generalized to
Alternative functors if we can
make sure to keep computability and universe polymorphism.