Generalise elimProp[n], elimContr[n], setQuotBinOp, etc in HITs.SetQuotients.Properties

[barrettj12]

Many lemmas in HITs.SetQuotients.Properties, notably elimProp[n], elimContr[n], and setQuot[n]Op, could be generalised so that:

• The quotient relation R doesn't have to have the same type as A
• When n > 1, the type family can depend on different quotients (e.g. C : A / R → B / S → Type ℓC

This is tedious work, but not particularly difficult, and it's useful. For example, when I was defining quotient categories, I couldn't use these lemmas, since they required the quotient types to all be the same. Hence I had to define operations/axioms on the quotient from scratch (using elimProp), which could have been avoided with more general versions.

I should also mention that the proofs are likely to be identical: only the type would be changed.

[mortberg]

I think this has been solved now, so closing