Up-to techniques are used to make it easier—or feasible—to construct, for instance, proofs of bisimilarity. This text shows how many up-to techniques can be framed as size-preserving functions, using sized types to keep track of sizes. Through a number of examples it is argued that this approach to up-to techniques is convenient to use in practice.

On the more theoretical side a class of up-to techniques intended to capture a natural mode of use of such size-preserving functions is defined. This class turns out to correspond closely to “functions below the companion”, a notion recently introduced by Pous.