Dan Licata and Guillaume Brunerie have an interesting paper on an agda-hott library for reasoning about cubical elements which appears to simplify some desired proofs: http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf
