actually fmap is what I meant instead of >>=
-rw-r--r-- 11 .gitignore
-rw-r--r-- 4453 Bidir.agda