This library was originally implemented by Pierre-Evariste Dagand and Conor McBride as part of their 'Transporting Functions Across Ornaments' paper (ICFP'2012). I've made some fixes to make Agda unification work with ornamented functions on non-trivially indexed types.

Unmodified code is available from Dagand's homepage:

http://gallium.inria.fr/~pdagand/stuffs/journal-2013-patch-jfp/model.tar.gz