Cf. the code in https://github.com/agda/agda/tree/master/notes/reflection developed during the Edinburgh AIM.