A port of the "Algebra of Programming Using
Dependent Types" [1] paper, using "setoid" rewriting
and type classes.

*Algebra of Programming Using Dependent Types*in

*Mathematics of Program Construction*. Shin-Cheng Mu, Hsiang-Shang Ko & Patrik Jansson. Philippe Audebaud and Christine Paulin-Mohring (Eds). Volume 5133 of