employ standard library of agda where possible
-rw-r--r-- 11 .gitignore
-rw-r--r-- 2314 Bidir.agda