[Agda] Filling squares

[James Wood]

Hi all,

I asked this question on IRC a few days ago, but it looks like no-one
there picked up on it. Perhaps it is more suited to the mailing list.

The question is explained fully in the code and comments of this file:
https://gist.github.com/laMudri/52d46ba2f385c3544b8bb6a05457c54a
To summarise, I'm using --cubical and being asked for a square which I
don't really know how to go about filling. I think it should be an
argument very similar to the contractibility of singletons, but I can't
piece it together.

Thanks,

James