New little Agda feature I'm cooking on the side (actually a second attempt...) got done enough in a day that I feel comfortable sharing the prototype:
https://github.com/agda/agda/pull/6669