Dependent sums and supporting typeclasses for comparing and formatting
them.