Did you tried to incorporate cubical agda into some real world development? For me it is cool to let internal machinery handle isomorphism between different types, but cubical agda library is still much smaller than std agda library ;/
The benefits look really promising e.g. proving forall x -> f x == g x -> f == g. I really want to use this theorem in some of my agda projects, but I never needed it desperately enough that I had to drop everything and do this. My usual workaround is implement slowButEasyToUnderstand function. Do a whole bunch of proofs with slowButEasyToUnderstand. Implement fastButComplicated function. Prove forall x slowButEasyToUnderstand x == fastButComplicated x
I think one immediate application I can think of with cubical is, you can implement mergeSort : List X -> List X and then pass this around everywhere. You don't need a Sorter record or whatever since when you implement quickSort, you will be able to prove quickSort == mergeSort, so everything will typecheck. I don't know which will end up getting compiled though.