first attempt to define bff (with holes)
-rw-r--r-- 11 .gitignore
-rw-r--r-- 2790 Bidir.agda