Algebra of Programming in Agda: Dependent Types for Relational Program Derivation - Mu, S; Ko, H; Jansson, P (Journal of Functional Programming, 2009)