Did you played with cubical flavor of Agda? here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2 :)