c.f. https://github.com/agda/agda/tree/master/notes/reflection
c.f. https://github.com/agda/agda/tree/master/notes/reflection