This is a port of the code from the paper Datatype-generic programming meets elaborator reflection, with the following modifications:
- The custom prelude has been replaced with a dependency on the Agda standard library.
- Anything irrelevant to the use of the library has been stripped out (i.e. code that may matter to a reader of the paper but is not likely to matter to a user of the library).
This is a work-in-progress; the claims above are not true yet.