At the Midlands Graduate School 2015, Venanzio Capretta gave a series of lectures and exercise classes on infinite data structures, with implementations in Haskell and Coq (the lecture notes and source code files are available on his website).
Some of the students who attended Venanzio's course wondered what the data structures and algorithms would look like in Agda. This repository contains what we cooked up.