Generalize quotient_kernel_factor, and use it in Ordinals.v

[jdchristensen]

It turns out that the image factorization for a function f to an h-set was already done in quotient_kernel_factor, and was even done in a way that let f x = f y be replaced by an equivalent relation R x y. Thus it was set-up to be used with propositional resizing, where R could be taken to have small values. I cleaned it up and provided this small version (as well as a version where R is definitionally f x = f y), and adapted Ordinal.v to use this instead of reproving it.

I left the factorization result in its bundled style. I don't love that, but it did make it easy to state variations quickly.

[Alizter]

It seems that 8.18 has different universe behaviour causing a build error.

[jdchristensen]

@Alizter This is ready for review now.