Interesting; I'll definitely take a closer look. In the mid-term, I'm hopeful that HoTT/cubical TT will render this issue obsolete. Short-term, I unfortunately can't rely on something this bleeding-edge (and I'd have to explain cubical type theory in the associated thesis, which is a little out of my league). Cheers, Jannis