A Cubical Agda case study, implementing an immutable FIFO queue using Higher Inductive Types to capture higher structure.
The queue is called BatchedQueue and is describe by Chris Okasaki in chapter 5.2 of his book Purely Functional Data Structures (Cambridge University Press, New York, NY, USA, 1999.).
The case study was a part of a project work done by @paldepind and @limemloh in Fall 2019.
Install Agda and the Cubical library using git.
In order to use the Cubical Agda in our files, we have created an .agda-lib describing cubical as a dependency.
To tell agda where to find the library, you need to add a path in a file ~/.agda/libraries, which you might have to create yourself.
The path to add is the one for the cubical.agda-lib found in the Cubical repo.
Such that ~/.agda/libraries look like this:
/path/to/cubical/cubical.agda-lib
Test by running C-c C-l in BatchedQueue.agda