Pointfree factorization of operation refinement

The standard operation refinement ordering is a kind of "meet of opposites": non-determinism reduction suggests "smaller" behaviour while increase of definition suggests "larger" behaviour. Groves' factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathematically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and exploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed.