opaque instead of abstract in QuotientAlgebra

[MatthiasHu]

This PR starts using the opaque feature of Agda 2.6.4 in the cubical library. Namely, it replaces the old abstract keyword in QuotientAlgebra.agda (where it was used to keep type checking times reasonable) with the new opaque/unfolding mechanism. I think the result is much cleaner and more readable than the old huge abstract block. (And also we could now use named modules again if we wanted!)

The transformation was straight-forward, none of the actual definitions had to be changed at all. (I only had to indent them one more level...)

I made a separate opaque block for every definition. This is I think recommendable because the way that definitions in the same opaque block can only be unfolded together can be confusing.

I am planning to do the same in FPAlgebra.agda, but thought it is good to start with small steps. :-)

[felixwellen]

Yes, it is good to start with small steps!
Looks good to me -> merging.